Axiom ax-his2 8905

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

Assertion

Ref	Expression
ax-his2	⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((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 8743	. . . 4 class ℋ
3	1, 2	wcel 957	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 957	. . 3 wff B ∈ ℋ
6		cC	. . . 4 class C
7	6, 2	wcel 957	. . 3 wff C ∈ ℋ
8	3, 5, 7	w3a 774	. 2 wff (A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ )
9		cva 8744	. . . . 5 class +h
10	1, 4, 9	co 3958	. . . 4 class (A +h B)
11		csp 8748	. . . 4 class ·ih
12	10, 6, 11	co 3958	. . 3 class ((A +h B) ·ih C)
13	1, 6, 11	co 3958	. . . 4 class (A ·ih C)
14	4, 6, 11	co 3958	. . . 4 class (B ·ih C)
15		caddc 5220	. . . 4 class +
16	13, 14, 15	co 3958	. . 3 class ((A ·ih C) + (B ·ih C))
17	12, 16	wceq 955	. 2 wff ((A +h B) ·ih C) = ((A ·ih C) + (B ·ih C))
18	8, 17	wi 3	1 wff ((A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A +h B) ·ih C) = ((A ·ih C) + (B ·ih C)))

This axiom is referenced by:  his7t 8911  hiassdit 8912  his2subt 8913  normlem0 8930  normlem8 8938  ocsh 9111  occllem1 9128  pjspansnt 9457  pjadj 9575  braaddt 9826  lnopunilem1 9891  hmopst 9901  cnlnadjlem2 9957  adjaddt 9982  leopaddt 10021

Copyright terms: Public domain