Axiom ax-his2 9099

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 8968	. . . 4 class H~
3	1, 2	wcel 1105	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 1105	. . 3 wff B e. H~
6		cC	. . . 4 class C
7	6, 2	wcel 1105	. . 3 wff C e. H~
8	3, 5, 7	w3a 772	. 2 wff (A e. H~ /\ B e. H~ /\ C e. H~)
9		cva 8969	. . . . 5 class +h
10	1, 4, 9	co 3902	. . . 4 class (A +h B)
11		csp 8973	. . . 4 class .ih
12	10, 6, 11	co 3902	. . 3 class ((A +h B) .ih C)
13	1, 6, 11	co 3902	. . . 4 class (A .ih C)
14	4, 6, 11	co 3902	. . . 4 class (B .ih C)
15		caddc 5160	. . . 4 class +
16	13, 14, 15	co 3902	. . 3 class ((A .ih C) + (B .ih C))
17	12, 16	wceq 1099	. 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:  his7t 9105  hiassdit 9106  his2subt 9107  normlem0 9124  normlem8 9132  ocsh 9286  occllem1 9303  pjspansnt 9631  pjadj 9749  braaddt 9999  lnopunilem1 10064  hmopst 10074  cnlnadjlem2 10130  adjaddt 10154  leopaddt 10191

Copyright terms: Public domain