Axiom ax-his3 31373

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 32139 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 11094	. . . 4 class ℂ
3	1, 2	wcel 2149	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31208	. . . 4 class ℋ
6	4, 5	wcel 2149	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2149	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1101	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31210	. . . . 5 class ·ℎ
11	1, 4, 10	co 7408	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31211	. . . 4 class ·ih
13	11, 7, 12	co 7408	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7408	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11101	. . . 4 class ·
16	1, 14, 15	co 7408	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1567	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31375  his35  31377  hiassdi  31380  his2sub  31381  hi01  31385  normlem0  31398  normlem9  31407  bcseqi  31409  polid2i  31446  ocsh  31572  h1de2i  31842  normcan  31865  eigrei  32123  eigorthi  32126  bramul  32235  lnopunilem1  32299  hmopm  32310  riesz3i  32351  cnlnadjlem2  32357  adjmul  32381  branmfn  32394  kbass2  32406  kbass5  32409  leopmuli  32422  leopnmid  32427