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 28788
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 29554 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 10523 . . . 4 class
31, 2wcel 2105 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chba 28623 . . . 4 class
64, 5wcel 2105 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2105 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1079 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28625 . . . . 5 class ·
111, 4, 10co 7145 . . . 4 class (𝐴 · 𝐵)
12 csp 28626 . . . 4 class ·ih
1311, 7, 12co 7145 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 7145 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10530 . . . 4 class ·
161, 14, 15co 7145 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1528 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  28790  his35  28792  hiassdi  28795  his2sub  28796  hi01  28800  normlem0  28813  normlem9  28822  bcseqi  28824  polid2i  28861  ocsh  28987  h1de2i  29257  normcan  29280  eigrei  29538  eigorthi  29541  bramul  29650  lnopunilem1  29714  hmopm  29725  riesz3i  29766  cnlnadjlem2  29772  adjmul  29796  branmfn  29809  kbass2  29821  kbass5  29824  leopmuli  29837  leopnmid  29842
  Copyright terms: Public domain W3C validator