Axiom ax-his3 29455

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 30221 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 10878	. . . 4 class ℂ
3	1, 2	wcel 2107	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 29290	. . . 4 class ℋ
6	4, 5	wcel 2107	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 29292	. . . . 5 class ·ℎ
11	1, 4, 10	co 7284	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 29293	. . . 4 class ·ih
13	11, 7, 12	co 7284	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7284	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10885	. . . 4 class ·
16	1, 14, 15	co 7284	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1539	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  29457  his35  29459  hiassdi  29462  his2sub  29463  hi01  29467  normlem0  29480  normlem9  29489  bcseqi  29491  polid2i  29528  ocsh  29654  h1de2i  29924  normcan  29947  eigrei  30205  eigorthi  30208  bramul  30317  lnopunilem1  30381  hmopm  30392  riesz3i  30433  cnlnadjlem2  30439  adjmul  30463  branmfn  30476  kbass2  30488  kbass5  30491  leopmuli  30504  leopnmid  30509