Axiom ax-his2 9226

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 9063	. . . 4 class H~
3	1, 2	wcel 994	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 994	. . 3 wff B e. H~
6		cC	. . . 4 class C
7	6, 2	wcel 994	. . 3 wff C e. H~
8	3, 5, 7	w3a 781	. 2 wff (A e. H~ /\ B e. H~ /\ C e. H~)
9		cva 9064	. . . . 5 class +h
10	1, 4, 9	co 4021	. . . 4 class (A +h B)
11		csp 9068	. . . 4 class .ih
12	10, 6, 11	co 4021	. . 3 class ((A +h B) .ih C)
13	1, 6, 11	co 4021	. . . 4 class (A .ih C)
14	4, 6, 11	co 4021	. . . 4 class (B .ih C)
15		caddc 5391	. . . 4 class +
16	13, 14, 15	co 4021	. . 3 class ((A .ih C) + (B .ih C))
17	12, 16	wceq 992	. 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 9232  hiassdi 9233  his2sub 9234  normlem0 9251  normlem8 9259  ocsh 9432  occllem1 9449  pjspansn 9776  pjadjii 9896  braadd 10149  lnopunilem1 10214  hmops 10224  cnlnadjlem2 10280  adjadd 10305  leopadd 10345

Copyright terms: Public domain