Axiom ax-his3 31013

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 31779 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 11066	. . . 4 class ℂ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30848	. . . 4 class ℋ
6	4, 5	wcel 2109	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2109	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30850	. . . . 5 class ·ℎ
11	1, 4, 10	co 7387	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30851	. . . 4 class ·ih
13	11, 7, 12	co 7387	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7387	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11073	. . . 4 class ·
16	1, 14, 15	co 7387	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1540	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31015  his35  31017  hiassdi  31020  his2sub  31021  hi01  31025  normlem0  31038  normlem9  31047  bcseqi  31049  polid2i  31086  ocsh  31212  h1de2i  31482  normcan  31505  eigrei  31763  eigorthi  31766  bramul  31875  lnopunilem1  31939  hmopm  31950  riesz3i  31991  cnlnadjlem2  31997  adjmul  32021  branmfn  32034  kbass2  32046  kbass5  32049  leopmuli  32062  leopnmid  32067