Axiom ax-his3 31695

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 32461 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 11205	. . . 4 class ℂ
3	1, 2	wcel 2144	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31530	. . . 4 class ℋ
6	4, 5	wcel 2144	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2144	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31532	. . . . 5 class ·ℎ
11	1, 4, 10	co 7424	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31533	. . . 4 class ·ih
13	11, 7, 12	co 7424	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7424	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11212	. . . 4 class ·
16	1, 14, 15	co 7424	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1569	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is used by:  his5  31697  his35  31699  hiassdi  31702  his2sub  31703  hi01  31707  normlem0  31720  normlem9  31729  bcseqi  31731  polid2i  31768  ocsh  31894  h1de2i  32164  normcan  32187  eigrei  32445  eigorthi  32448  bramul  32557  lnopunilem1  32621  hmopm  32632  riesz3i  32673  cnlnadjlem2  32679  adjmul  32703  branmfn  32716  kbass2  32728  kbass5  32731  leopmuli  32744  leopnmid  32749