Axiom ax-his3 31743

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 32509 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 11237	. . . 4 class ℂ
3	1, 2	wcel 2147	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31578	. . . 4 class ℋ
6	4, 5	wcel 2147	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2147	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31580	. . . . 5 class ·ℎ
11	1, 4, 10	co 7451	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31581	. . . 4 class ·ih
13	11, 7, 12	co 7451	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7451	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11244	. . . 4 class ·
16	1, 14, 15	co 7451	. . 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  31745  his35  31747  hiassdi  31750  his2sub  31751  hi01  31755  normlem0  31768  normlem9  31777  bcseqi  31779  polid2i  31816  ocsh  31942  h1de2i  32212  normcan  32235  eigrei  32493  eigorthi  32496  bramul  32605  lnopunilem1  32669  hmopm  32680  riesz3i  32721  cnlnadjlem2  32727  adjmul  32751  branmfn  32764  kbass2  32776  kbass5  32779  leopmuli  32792  leopnmid  32797