Axiom ax-his2 8950

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 8788	. . . 4 class H~
3	1, 2	wcel 958	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 958	. . 3 wff B e. H~
6		cC	. . . 4 class C
7	6, 2	wcel 958	. . 3 wff C e. H~
8	3, 5, 7	w3a 775	. 2 wff (A e. H~ /\ B e. H~ /\ C e. H~)
9		cva 8789	. . . . 5 class +h
10	1, 4, 9	co 3963	. . . 4 class (A +h B)
11		csp 8793	. . . 4 class .ih
12	10, 6, 11	co 3963	. . 3 class ((A +h B) .ih C)
13	1, 6, 11	co 3963	. . . 4 class (A .ih C)
14	4, 6, 11	co 3963	. . . 4 class (B .ih C)
15		caddc 5237	. . . 4 class +
16	13, 14, 15	co 3963	. . 3 class ((A .ih C) + (B .ih C))
17	12, 16	wceq 956	. 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 8956  hiassdit 8957  his2subt 8958  normlem0 8975  normlem8 8983  ocsh 9156  occllem1 9173  pjspansnt 9500  pjadj 9618  braaddt 9869  lnopunilem1 9935  hmopst 9945  cnlnadjlem2 10001  adjaddt 10026  leopaddt 10065

Copyright terms: Public domain