Axiom ax-his3 30986

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 31752 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 11042	. . . 4 class ℂ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30821	. . . 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 30823	. . . . 5 class ·ℎ
11	1, 4, 10	co 7369	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30824	. . . 4 class ·ih
13	11, 7, 12	co 7369	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7369	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11049	. . . 4 class ·
16	1, 14, 15	co 7369	. . 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  30988  his35  30990  hiassdi  30993  his2sub  30994  hi01  30998  normlem0  31011  normlem9  31020  bcseqi  31022  polid2i  31059  ocsh  31185  h1de2i  31455  normcan  31478  eigrei  31736  eigorthi  31739  bramul  31848  lnopunilem1  31912  hmopm  31923  riesz3i  31964  cnlnadjlem2  31970  adjmul  31994  branmfn  32007  kbass2  32019  kbass5  32022  leopmuli  32035  leopnmid  32040