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 27911
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 28679 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 9919 . . . 4 class
31, 2wcel 1988 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chil 27746 . . . 4 class
64, 5wcel 1988 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 1988 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1036 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 27748 . . . . 5 class ·
111, 4, 10co 6635 . . . 4 class (𝐴 · 𝐵)
12 csp 27749 . . . 4 class ·ih
1311, 7, 12co 6635 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 6635 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 9926 . . . 4 class ·
161, 14, 15co 6635 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1481 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  27913  his35  27915  hiassdi  27918  his2sub  27919  hi01  27923  normlem0  27936  normlem9  27945  bcseqi  27947  polid2i  27984  ocsh  28112  h1de2i  28382  normcan  28405  eigrei  28663  eigorthi  28666  bramul  28775  lnopunilem1  28839  hmopm  28850  riesz3i  28891  cnlnadjlem2  28897  adjmul  28921  branmfn  28934  kbass2  28946  kbass5  28949  leopmuli  28962  leopnmid  28967
  Copyright terms: Public domain W3C validator