Axiom ax-his3 28861

Description: Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (𝐵 ·_ih (𝐴 ·_ℎ 𝐶)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 29627 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-his3	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cc 10535	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 28696	. . . 4 class ℋ
6	4, 5	wcel 2114	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1083	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28698	. . . . 5 class ·ℎ
11	1, 4, 10	co 7156	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28699	. . . 4 class ·ih
13	11, 7, 12	co 7156	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7156	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10542	. . . 4 class ·
16	1, 14, 15	co 7156	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1537	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28863  his35  28865  hiassdi  28868  his2sub  28869  hi01  28873  normlem0  28886  normlem9  28895  bcseqi  28897  polid2i  28934  ocsh  29060  h1de2i  29330  normcan  29353  eigrei  29611  eigorthi  29614  bramul  29723  lnopunilem1  29787  hmopm  29798  riesz3i  29839  cnlnadjlem2  29845  adjmul  29869  branmfn  29882  kbass2  29894  kbass5  29897  leopmuli  29910  leopnmid  29915