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

Theorem his1i 27147
Description: Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
his1.1 𝐴 ∈ ℋ
his1.2 𝐵 ∈ ℋ
Assertion
Ref Expression
his1i (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))

Proof of Theorem his1i
StepHypRef Expression
1 his1.1 . 2 𝐴 ∈ ℋ
2 his1.2 . 2 𝐵 ∈ ℋ
3 ax-his1 27129 . 2 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴)))
41, 2, 3mp2an 703 1 (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  cfv 5790  (class class class)co 6527  ccj 13630  chil 26966   ·ih csp 26969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-his1 27129
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  normlem2  27158  bcseqi  27167  bcsiALT  27226  pjadjii  27723  lnopunilem1  28059  lnophmlem2  28066
  Copyright terms: Public domain W3C validator