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 28789
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 29555 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 10524 . . . 4 class
31, 2wcel 2105 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chba 28624 . . . 4 class
64, 5wcel 2105 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2105 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1079 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28626 . . . . 5 class ·
111, 4, 10co 7145 . . . 4 class (𝐴 · 𝐵)
12 csp 28627 . . . 4 class ·ih
1311, 7, 12co 7145 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 7145 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10531 . . . 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  28791  his35  28793  hiassdi  28796  his2sub  28797  hi01  28801  normlem0  28814  normlem9  28823  bcseqi  28825  polid2i  28862  ocsh  28988  h1de2i  29258  normcan  29281  eigrei  29539  eigorthi  29542  bramul  29651  lnopunilem1  29715  hmopm  29726  riesz3i  29767  cnlnadjlem2  29773  adjmul  29797  branmfn  29810  kbass2  29822  kbass5  29825  leopmuli  29838  leopnmid  29843
  Copyright terms: Public domain W3C validator