Axiom ax-his3 31507

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 32273 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 11113	. . . 4 class ℂ
3	1, 2	wcel 2146	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31342	. . . 4 class ℋ
6	4, 5	wcel 2146	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2146	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31344	. . . . 5 class ·ℎ
11	1, 4, 10	co 7419	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31345	. . . 4 class ·ih
13	11, 7, 12	co 7419	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7419	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11120	. . . 4 class ·
16	1, 14, 15	co 7419	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1570	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is used by:  his5  31509  his35  31511  hiassdi  31514  his2sub  31515  hi01  31519  normlem0  31532  normlem9  31541  bcseqi  31543  polid2i  31580  ocsh  31706  h1de2i  31976  normcan  31999  eigrei  32257  eigorthi  32260  bramul  32369  lnopunilem1  32433  hmopm  32444  riesz3i  32485  cnlnadjlem2  32491  adjmul  32515  branmfn  32528  kbass2  32540  kbass5  32543  leopmuli  32556  leopnmid  32561