Axiom ax-his3 28281

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 29049 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 10136	. . . 4 class ℂ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chil 28116	. . . 4 class ℋ
6	4, 5	wcel 2145	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2145	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1071	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28118	. . . . 5 class ·ℎ
11	1, 4, 10	co 6793	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28119	. . . 4 class ·ih
13	11, 7, 12	co 6793	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 6793	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10143	. . . 4 class ·
16	1, 14, 15	co 6793	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1631	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28283  his35  28285  hiassdi  28288  his2sub  28289  hi01  28293  normlem0  28306  normlem9  28315  bcseqi  28317  polid2i  28354  ocsh  28482  h1de2i  28752  normcan  28775  eigrei  29033  eigorthi  29036  bramul  29145  lnopunilem1  29209  hmopm  29220  riesz3i  29261  cnlnadjlem2  29267  adjmul  29291  branmfn  29304  kbass2  29316  kbass5  29319  leopmuli  29332  leopnmid  29337