Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-his3 Structured version   Visualization version   GIF version

Axiom ax-his3 28221
 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 28989 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 10097 . . . 4 class
31, 2wcel 2127 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chil 28056 . . . 4 class
64, 5wcel 2127 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2127 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1072 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28058 . . . . 5 class ·
111, 4, 10co 6801 . . . 4 class (𝐴 · 𝐵)
12 csp 28059 . . . 4 class ·ih
1311, 7, 12co 6801 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 6801 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10104 . . . 4 class ·
161, 14, 15co 6801 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1620 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
 Colors of variables: wff setvar class This axiom is referenced by:  his5  28223  his35  28225  hiassdi  28228  his2sub  28229  hi01  28233  normlem0  28246  normlem9  28255  bcseqi  28257  polid2i  28294  ocsh  28422  h1de2i  28692  normcan  28715  eigrei  28973  eigorthi  28976  bramul  29085  lnopunilem1  29149  hmopm  29160  riesz3i  29201  cnlnadjlem2  29207  adjmul  29231  branmfn  29244  kbass2  29256  kbass5  29259  leopmuli  29272  leopnmid  29277
 Copyright terms: Public domain W3C validator