Axiom ax-hvdistr1 8833

Description: Scalar multiplication distributive law

Assertion

Ref	Expression
ax-hvdistr1	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .h (B +h C)) = ((A .h B) +h (A .h C)))

Detailed syntax breakdown of Axiom ax-hvdistr1

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 5220	. . . 4 class CC
3	1, 2	wcel 958	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 8743	. . . 4 class H~
6	4, 5	wcel 958	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 958	. . 3 wff C e. H~
9	3, 6, 8	w3a 775	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		cva 8744	. . . . 5 class +h
11	4, 7, 10	co 3961	. . . 4 class (B +h C)
12		csm 8745	. . . 4 class .h
13	1, 11, 12	co 3961	. . 3 class (A .h (B +h C))
14	1, 4, 12	co 3961	. . . 4 class (A .h B)
15	1, 7, 12	co 3961	. . . 4 class (A .h C)
16	14, 15, 10	co 3961	. . 3 class ((A .h B) +h (A .h C))
17	13, 16	wceq 956	. 2 wff (A .h (B +h C)) = ((A .h B) +h (A .h C))
18	9, 17	wi 3	1 wff ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .h (B +h C)) = ((A .h B) +h (A .h C)))

This axiom is referenced by:  hvsub4t 8861  hvsubdistr1t 8871  hvdistr1 8873  hv2timest 8883  hilvc 8984  hhssnv 9089  shscl 9236  spanunsn 9457  hoadddit 9684  lnopm 9880  lnophs 9881

Copyright terms: Public domain