Axiom ax-his2 8952

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 8790	. . . 4 class H~
3	1, 2	wcel 960	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 960	. . 3 wff B e. H~
6		cC	. . . 4 class C
7	6, 2	wcel 960	. . 3 wff C e. H~
8	3, 5, 7	w3a 777	. 2 wff (A e. H~ /\ B e. H~ /\ C e. H~)
9		cva 8791	. . . . 5 class +h
10	1, 4, 9	co 3970	. . . 4 class (A +h B)
11		csp 8795	. . . 4 class .ih
12	10, 6, 11	co 3970	. . 3 class ((A +h B) .ih C)
13	1, 6, 11	co 3970	. . . 4 class (A .ih C)
14	4, 6, 11	co 3970	. . . 4 class (B .ih C)
15		caddc 5256	. . . 4 class +
16	13, 14, 15	co 3970	. . 3 class ((A .ih C) + (B .ih C))
17	12, 16	wceq 958	. 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 8958  hiassdit 8959  his2subt 8960  normlem0 8977  normlem8 8985  ocsh 9158  occllem1 9175  pjspansnt 9502  pjadj 9620  braaddt 9871  lnopunilem1 9937  hmopst 9947  cnlnadjlem2 10003  adjaddt 10028  leopaddt 10067

Copyright terms: Public domain