Axiom ax-his2 8871

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 8727	. . . 4 class ℋ
3	1, 2	wcel 955	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 955	. . 3 wff B ∈ ℋ
6		cC	. . . 4 class C
7	6, 2	wcel 955	. . 3 wff C ∈ ℋ
8	3, 5, 7	w3a 773	. 2 wff (A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ )
9		cva 8728	. . . . 5 class +h
10	1, 4, 9	co 3948	. . . 4 class (A +h B)
11		csp 8732	. . . 4 class ·ih
12	10, 6, 11	co 3948	. . 3 class ((A +h B) ·ih C)
13	1, 6, 11	co 3948	. . . 4 class (A ·ih C)
14	4, 6, 11	co 3948	. . . 4 class (B ·ih C)
15		caddc 5209	. . . 4 class +
16	13, 14, 15	co 3948	. . 3 class ((A ·ih C) + (B ·ih C))
17	12, 16	wceq 953	. 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 8877  hiassdit 8878  his2subt 8879  normlem0 8896  normlem8 8904  ocsh 9072  occllem1 9089  pjspansnt 9417  pjadj 9535  braaddt 9785  lnopunilem1 9850  hmopst 9860  cnlnadjlem2 9916  adjaddt 9940  leopaddt 9977

Copyright terms: Public domain