Axiom ax-his3 31170

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 31936 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 11027	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31005	. . . 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 31007	. . . . 5 class ·ℎ
11	1, 4, 10	co 7360	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31008	. . . 4 class ·ih
13	11, 7, 12	co 7360	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7360	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11034	. . . 4 class ·
16	1, 14, 15	co 7360	. . 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  31172  his35  31174  hiassdi  31177  his2sub  31178  hi01  31182  normlem0  31195  normlem9  31204  bcseqi  31206  polid2i  31243  ocsh  31369  h1de2i  31639  normcan  31662  eigrei  31920  eigorthi  31923  bramul  32032  lnopunilem1  32096  hmopm  32107  riesz3i  32148  cnlnadjlem2  32154  adjmul  32178  branmfn  32191  kbass2  32203  kbass5  32206  leopmuli  32219  leopnmid  32224