Axiom ax-hvdistr2 10511

Description: Scalar multiplication distributive law.

Assertion

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

Detailed syntax breakdown of Axiom ax-hvdistr2

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 6384	. . . 4 class CC
3	1, 2	wcel 1300	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 1300	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 10420	. . . 4 class ~H
8	6, 7	wcel 1300	. . 3 wff C e. ~H
9	3, 5, 8	w3a 858	. 2 wff (A e. CC /\ B e. CC /\ C e. ~H)
10		caddc 6389	. . . . 5 class +
11	1, 4, 10	co 4884	. . . 4 class (A + B)
12		csm 10422	. . . 4 class .h
13	11, 6, 12	co 4884	. . 3 class ((A + B) .h C)
14	1, 6, 12	co 4884	. . . 4 class (A .h C)
15	4, 6, 12	co 4884	. . . 4 class (B .h C)
16		cva 10421	. . . 4 class +h
17	14, 15, 16	co 4884	. . 3 class ((A .h C) +h (B .h C))
18	13, 17	wceq 1298	. 2 wff ((A + B) .h C) = ((A .h C) +h (B .h C))
19	9, 18	wi 3	1 wff ((A e. CC /\ B e. CC /\ C e. ~H) -> ((A + B) .h C) = ((A .h C) +h (B .h C)))

This axiom is referenced by:  hvsubid 10527  hvsubdistr2 10549  hv2times 10560  hilvc 10662  hhssnv 10767  hoadddir 11367  superpos 11926

Copyright terms: Public domain