Axiom ax-his3 31155

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 31921 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 11036	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30990	. . . 4 class ℋ
6	4, 5	wcel 2114	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30992	. . . . 5 class ·ℎ
11	1, 4, 10	co 7367	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30993	. . . 4 class ·ih
13	11, 7, 12	co 7367	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7367	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11043	. . . 4 class ·
16	1, 14, 15	co 7367	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1542	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31157  his35  31159  hiassdi  31162  his2sub  31163  hi01  31167  normlem0  31180  normlem9  31189  bcseqi  31191  polid2i  31228  ocsh  31354  h1de2i  31624  normcan  31647  eigrei  31905  eigorthi  31908  bramul  32017  lnopunilem1  32081  hmopm  32092  riesz3i  32133  cnlnadjlem2  32139  adjmul  32163  branmfn  32176  kbass2  32188  kbass5  32191  leopmuli  32204  leopnmid  32209