Axiom ax-his3 31687

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 32453 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 11199	. . . 4 class ℂ
3	1, 2	wcel 2144	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31522	. . . 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 31524	. . . . 5 class ·ℎ
11	1, 4, 10	co 7420	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31525	. . . 4 class ·ih
13	11, 7, 12	co 7420	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7420	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11206	. . . 4 class ·
16	1, 14, 15	co 7420	. . 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  31689  his35  31691  hiassdi  31694  his2sub  31695  hi01  31699  normlem0  31712  normlem9  31721  bcseqi  31723  polid2i  31760  ocsh  31886  h1de2i  32156  normcan  32179  eigrei  32437  eigorthi  32440  bramul  32549  lnopunilem1  32613  hmopm  32624  riesz3i  32665  cnlnadjlem2  32671  adjmul  32695  branmfn  32708  kbass2  32720  kbass5  32723  leopmuli  32736  leopnmid  32741