HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-his3 Structured version   Visualization version   GIF version

Axiom ax-his3 28281
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 29049 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
StepHypRef Expression
1 cA . . . 4 class 𝐴
2 cc 10136 . . . 4 class
31, 2wcel 2145 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chil 28116 . . . 4 class
64, 5wcel 2145 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2145 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1071 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28118 . . . . 5 class ·
111, 4, 10co 6793 . . . 4 class (𝐴 · 𝐵)
12 csp 28119 . . . 4 class ·ih
1311, 7, 12co 6793 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 6793 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10143 . . . 4 class ·
161, 14, 15co 6793 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1631 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  28283  his35  28285  hiassdi  28288  his2sub  28289  hi01  28293  normlem0  28306  normlem9  28315  bcseqi  28317  polid2i  28354  ocsh  28482  h1de2i  28752  normcan  28775  eigrei  29033  eigorthi  29036  bramul  29145  lnopunilem1  29209  hmopm  29220  riesz3i  29261  cnlnadjlem2  29267  adjmul  29291  branmfn  29304  kbass2  29316  kbass5  29319  leopmuli  29332  leopnmid  29337
  Copyright terms: Public domain W3C validator