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 27325
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 28093 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 9813 . . . 4 class
31, 2wcel 1977 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chil 27160 . . . 4 class
64, 5wcel 1977 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 1977 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1031 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 27162 . . . . 5 class ·
111, 4, 10co 6549 . . . 4 class (𝐴 · 𝐵)
12 csp 27163 . . . 4 class ·ih
1311, 7, 12co 6549 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 6549 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 9820 . . . 4 class ·
161, 14, 15co 6549 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1475 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  27327  his35  27329  hiassdi  27332  his2sub  27333  hi01  27337  normlem0  27350  normlem9  27359  bcseqi  27361  polid2i  27398  ocsh  27526  h1de2i  27796  normcan  27819  eigrei  28077  eigorthi  28080  bramul  28189  lnopunilem1  28253  hmopm  28264  riesz3i  28305  cnlnadjlem2  28311  adjmul  28335  branmfn  28348  kbass2  28360  kbass5  28363  leopmuli  28376  leopnmid  28381
  Copyright terms: Public domain W3C validator