Axiom ax-his3 31116

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 31882 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 11182	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30951	. . . 4 class ℋ
6	4, 5	wcel 2108	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2108	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30953	. . . . 5 class ·ℎ
11	1, 4, 10	co 7448	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30954	. . . 4 class ·ih
13	11, 7, 12	co 7448	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7448	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11189	. . . 4 class ·
16	1, 14, 15	co 7448	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1537	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31118  his35  31120  hiassdi  31123  his2sub  31124  hi01  31128  normlem0  31141  normlem9  31150  bcseqi  31152  polid2i  31189  ocsh  31315  h1de2i  31585  normcan  31608  eigrei  31866  eigorthi  31869  bramul  31978  lnopunilem1  32042  hmopm  32053  riesz3i  32094  cnlnadjlem2  32100  adjmul  32124  branmfn  32137  kbass2  32149  kbass5  32152  leopmuli  32165  leopnmid  32170