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

Theorem his1i 28085
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 28067 . 2 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴)))
41, 2, 3mp2an 708 1 (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  cfv 5926  (class class class)co 6690  ccj 13880  chil 27904   ·ih csp 27907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-his1 28067
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  normlem2  28096  bcseqi  28105  bcsiALT  28164  pjadjii  28661  lnopunilem1  28997  lnophmlem2  29004
  Copyright terms: Public domain W3C validator