Axiom ax-his3 31011

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 31777 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 11125	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30846	. . . 4 class ℋ
6	4, 5	wcel 2108	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2108	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30848	. . . . 5 class ·ℎ
11	1, 4, 10	co 7403	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30849	. . . 4 class ·ih
13	11, 7, 12	co 7403	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7403	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11132	. . . 4 class ·
16	1, 14, 15	co 7403	. . 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  31013  his35  31015  hiassdi  31018  his2sub  31019  hi01  31023  normlem0  31036  normlem9  31045  bcseqi  31047  polid2i  31084  ocsh  31210  h1de2i  31480  normcan  31503  eigrei  31761  eigorthi  31764  bramul  31873  lnopunilem1  31937  hmopm  31948  riesz3i  31989  cnlnadjlem2  31995  adjmul  32019  branmfn  32032  kbass2  32044  kbass5  32047  leopmuli  32060  leopnmid  32065