Axiom ax-his3 5047

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

Assertion

Ref	Expression
ax-his3	⊢ ((A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A ·s B) ·i C) = (A · (B ·i C)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 4026	. . . 4 class ℂ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5		chil 4958	. . . 4 class ℋ
6	4, 5	wcel 1092	. . 3 wff B ∈ ℋ
7		cC	. . . 4 class C
8	7, 5	wcel 1092	. . 3 wff C ∈ ℋ
9	3, 6, 8	w3a 581	. 2 wff (A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ )
10		csm 4960	. . . . 5 class ·s
11	1, 4, 10	co 3001	. . . 4 class (A ·s B)
12		csp 4963	. . . 4 class ·i
13	11, 7, 12	co 3001	. . 3 class ((A ·s B) ·i C)
14	4, 7, 12	co 3001	. . . 4 class (B ·i C)
15		cmulc 4032	. . . 4 class ·
16	1, 14, 15	co 3001	. . 3 class (A · (B ·i C))
17	13, 16	wceq 1091	. 2 wff ((A ·s B) ·i C) = (A · (B ·i C))
18	9, 17	wi 2	1 wff ((A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A ·s B) ·i C) = (A · (B ·i C)))

This axiom is referenced by:  his5 5050  his2subt 5052  hizer1t 5054  normlem0 5062  normlem8 5071  bcseq 5073  norm-iii 5087  ocsh 5164  occllem1 5180  h1de2 5458

metamath.org