Axiom ax-his2 10375

Description: Distributive law for inner product. Postulate (S2) of [Beran] p. 95.

Assertion

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

Detailed syntax breakdown of Axiom ax-his2

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 10212	. . . 4 class ~H
3	1, 2	wcel 1138	. . 3 wff A e. ~H
4		cB	. . . 4 class B
5	4, 2	wcel 1138	. . 3 wff B e. ~H
6		cC	. . . 4 class C
7	6, 2	wcel 1138	. . 3 wff C e. ~H
8	3, 5, 7	w3a 855	. 2 wff (A e. ~H /\ B e. ~H /\ C e. ~H)
9		cva 10213	. . . . 5 class +h
10	1, 4, 9	co 4695	. . . 4 class (A +h B)
11		csp 10217	. . . 4 class .ih
12	10, 6, 11	co 4695	. . 3 class ((A +h B) .ih C)
13	1, 6, 11	co 4695	. . . 4 class (A .ih C)
14	4, 6, 11	co 4695	. . . 4 class (B .ih C)
15		caddc 6185	. . . 4 class +
16	13, 14, 15	co 4695	. . 3 class ((A .ih C) + (B .ih C))
17	12, 16	wceq 1136	. 2 wff ((A +h B) .ih C) = ((A .ih C) + (B .ih C))
18	8, 17	wi 3	1 wff ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A +h B) .ih C) = ((A .ih C) + (B .ih C)))

This axiom is referenced by:  his7 10381  hiassdi 10382  his2sub 10383  normlem0 10400  normlem8 10408  ocsh 10581  occllem1 10598  pjspansn 10925  pjadjii 11045  braadd 11298  lnopunilem1 11364  hmops 11374  cnlnadjlem2 11430  adjadd 11455  leopadd 11495

Copyright terms: Public domain