Axiom ax-his3 30315

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 31081 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 11104	. . . 4 class ℂ
3	1, 2	wcel 2107	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30150	. . . 4 class ℋ
6	4, 5	wcel 2107	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1088	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30152	. . . . 5 class ·ℎ
11	1, 4, 10	co 7404	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30153	. . . 4 class ·ih
13	11, 7, 12	co 7404	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7404	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11111	. . . 4 class ·
16	1, 14, 15	co 7404	. . 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  30317  his35  30319  hiassdi  30322  his2sub  30323  hi01  30327  normlem0  30340  normlem9  30349  bcseqi  30351  polid2i  30388  ocsh  30514  h1de2i  30784  normcan  30807  eigrei  31065  eigorthi  31068  bramul  31177  lnopunilem1  31241  hmopm  31252  riesz3i  31293  cnlnadjlem2  31299  adjmul  31323  branmfn  31336  kbass2  31348  kbass5  31351  leopmuli  31364  leopnmid  31369