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 28860
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 29626 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 10534 . . . 4 class
31, 2wcel 2110 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chba 28695 . . . 4 class
64, 5wcel 2110 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2110 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1083 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28697 . . . . 5 class ·
111, 4, 10co 7155 . . . 4 class (𝐴 · 𝐵)
12 csp 28698 . . . 4 class ·ih
1311, 7, 12co 7155 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 7155 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10541 . . . 4 class ·
161, 14, 15co 7155 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1533 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  28862  his35  28864  hiassdi  28867  his2sub  28868  hi01  28872  normlem0  28885  normlem9  28894  bcseqi  28896  polid2i  28933  ocsh  29059  h1de2i  29329  normcan  29352  eigrei  29610  eigorthi  29613  bramul  29722  lnopunilem1  29786  hmopm  29797  riesz3i  29838  cnlnadjlem2  29844  adjmul  29868  branmfn  29881  kbass2  29893  kbass5  29896  leopmuli  29909  leopnmid  29914
  Copyright terms: Public domain W3C validator