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

Axiom ax-his3 28959
 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 29725 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 10566 . . . 4 class
31, 2wcel 2112 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chba 28794 . . . 4 class
64, 5wcel 2112 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 2112 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1085 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 28796 . . . . 5 class ·
111, 4, 10co 7151 . . . 4 class (𝐴 · 𝐵)
12 csp 28797 . . . 4 class ·ih
1311, 7, 12co 7151 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 7151 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 10573 . . . 4 class ·
161, 14, 15co 7151 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1539 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
 Colors of variables: wff setvar class This axiom is referenced by:  his5  28961  his35  28963  hiassdi  28966  his2sub  28967  hi01  28971  normlem0  28984  normlem9  28993  bcseqi  28995  polid2i  29032  ocsh  29158  h1de2i  29428  normcan  29451  eigrei  29709  eigorthi  29712  bramul  29821  lnopunilem1  29885  hmopm  29896  riesz3i  29937  cnlnadjlem2  29943  adjmul  29967  branmfn  29980  kbass2  29992  kbass5  29995  leopmuli  30008  leopnmid  30013
 Copyright terms: Public domain W3C validator