Axiom ax-his2 5046

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

Assertion

Ref	Expression
ax-his2	⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A +v B) ·i C) = ((A ·i C) + (B ·i C)))

Detailed syntax breakdown of Axiom ax-his2

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class ℋ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B ∈ ℋ
6		cC	. . . 4 class C
7	6, 2	wcel 1092	. . 3 wff C ∈ ℋ
8	3, 5, 7	w3a 581	. 2 wff (A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ )
9		cva 4959	. . . . 5 class +v
10	1, 4, 9	co 3001	. . . 4 class (A +v B)
11		csp 4963	. . . 4 class ·i
12	10, 6, 11	co 3001	. . 3 class ((A +v B) ·i C)
13	1, 6, 11	co 3001	. . . 4 class (A ·i C)
14	4, 6, 11	co 3001	. . . 4 class (B ·i C)
15		caddc 4031	. . . 4 class +
16	13, 14, 15	co 3001	. . 3 class ((A ·i C) + (B ·i C))
17	12, 16	wceq 1091	. 2 wff ((A +v B) ·i C) = ((A ·i C) + (B ·i C))
18	8, 17	wi 2	1 wff ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A +v B) ·i C) = ((A ·i C) + (B ·i C)))

This axiom is referenced by:  his7 5051  his2subt 5052  normlem0 5062  normlem9 5070  norm-ii 5086  ocsh 5164  occllem1 5180  pjadj 5564

metamath.org