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 30302
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 31068 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 11095 . . . 4 class
31, 2wcel 2107 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chba 30137 . . . 4 class
64, 5wcel 2107 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2107 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1088 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 30139 . . . . 5 class ·
111, 4, 10co 7396 . . . 4 class (𝐴 · 𝐵)
12 csp 30140 . . . 4 class ·ih
1311, 7, 12co 7396 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 7396 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 11102 . . . 4 class ·
161, 14, 15co 7396 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1542 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  30304  his35  30306  hiassdi  30309  his2sub  30310  hi01  30314  normlem0  30327  normlem9  30336  bcseqi  30338  polid2i  30375  ocsh  30501  h1de2i  30771  normcan  30794  eigrei  31052  eigorthi  31055  bramul  31164  lnopunilem1  31228  hmopm  31239  riesz3i  31280  cnlnadjlem2  31286  adjmul  31310  branmfn  31323  kbass2  31335  kbass5  31338  leopmuli  31351  leopnmid  31356
  Copyright terms: Public domain W3C validator