Axiom ax-his3 31565

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 32331 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 11122	. . . 4 class ℂ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31400	. . . 4 class ℋ
6	4, 5	wcel 2145	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2145	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31402	. . . . 5 class ·ℎ
11	1, 4, 10	co 7413	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31403	. . . 4 class ·ih
13	11, 7, 12	co 7413	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7413	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11129	. . . 4 class ·
16	1, 14, 15	co 7413	. . 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  31567  his35  31569  hiassdi  31572  his2sub  31573  hi01  31577  normlem0  31590  normlem9  31599  bcseqi  31601  polid2i  31638  ocsh  31764  h1de2i  32034  normcan  32057  eigrei  32315  eigorthi  32318  bramul  32427  lnopunilem1  32491  hmopm  32502  riesz3i  32543  cnlnadjlem2  32549  adjmul  32573  branmfn  32586  kbass2  32598  kbass5  32601  leopmuli  32614  leopnmid  32619