Axiom ax-his3 31020

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 31786 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 11073	. . . 4 class ℂ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30855	. . . 4 class ℋ
6	4, 5	wcel 2109	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2109	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30857	. . . . 5 class ·ℎ
11	1, 4, 10	co 7390	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30858	. . . 4 class ·ih
13	11, 7, 12	co 7390	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7390	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11080	. . . 4 class ·
16	1, 14, 15	co 7390	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1540	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31022  his35  31024  hiassdi  31027  his2sub  31028  hi01  31032  normlem0  31045  normlem9  31054  bcseqi  31056  polid2i  31093  ocsh  31219  h1de2i  31489  normcan  31512  eigrei  31770  eigorthi  31773  bramul  31882  lnopunilem1  31946  hmopm  31957  riesz3i  31998  cnlnadjlem2  32004  adjmul  32028  branmfn  32041  kbass2  32053  kbass5  32056  leopmuli  32069  leopnmid  32074