Axiom ax-hvdistr1 27865

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)

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 9934	. . . 4 class CC
3	1, 2	wcel 1990	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 27776	. . . 4 class ~H
6	4, 5	wcel 1990	. . 3 wff B e. ~H
7		cC	. . . 4 class C
8	7, 5	wcel 1990	. . 3 wff C e. ~H
9	3, 6, 8	w3a 1037	. 2 wff ( A e. CC /\ B e. ~H /\ C e. ~H )
10		cva 27777	. . . . 5 class +h
11	4, 7, 10	co 6650	. . . 4 class ( B +h C )
12		csm 27778	. . . 4 class .h
13	1, 11, 12	co 6650	. . 3 class ( A .h ( B +h C ) )
14	1, 4, 12	co 6650	. . . 4 class ( A .h B )
15	1, 7, 12	co 6650	. . . 4 class ( A .h C )
16	14, 15, 10	co 6650	. . 3 class ( ( A .h B ) +h ( A .h C ) )
17	13, 16	wceq 1483	. 2 wff ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) )
18	9, 17	wi 4	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:  hvsub4  27894  hvsubass  27901  hvsubdistr1  27906  hvdistr1i  27908  hv2times  27918  hilvc  28019  hhssnv  28121  shscli  28176  spanunsni  28438  hoadddi  28662  lnopmi  28859  lnophsi  28860