Axiom ax-his3 28485

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 29253 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 10250	. . . 4 class ℂ
3	1, 2	wcel 2164	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 28320	. . . 4 class ℋ
6	4, 5	wcel 2164	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2164	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1111	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28322	. . . . 5 class ·ℎ
11	1, 4, 10	co 6905	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28323	. . . 4 class ·ih
13	11, 7, 12	co 6905	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 6905	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10257	. . . 4 class ·
16	1, 14, 15	co 6905	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1656	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28487  his35  28489  hiassdi  28492  his2sub  28493  hi01  28497  normlem0  28510  normlem9  28519  bcseqi  28521  polid2i  28558  ocsh  28686  h1de2i  28956  normcan  28979  eigrei  29237  eigorthi  29240  bramul  29349  lnopunilem1  29413  hmopm  29424  riesz3i  29465  cnlnadjlem2  29471  adjmul  29495  branmfn  29508  kbass2  29520  kbass5  29523  leopmuli  29536  leopnmid  29541