Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  leopg Unicode version

Theorem leopg 23545
 Description: Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
Assertion
Ref Expression
leopg
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem leopg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6042 . . . 4
21eleq1d 2467 . . 3
31fveq1d 5684 . . . . . 6
43oveq1d 6049 . . . . 5
54breq2d 4179 . . . 4
65ralbidv 2683 . . 3
72, 6anbi12d 692 . 2
8 oveq1 6041 . . . 4
98eleq1d 2467 . . 3
108fveq1d 5684 . . . . . 6
1110oveq1d 6049 . . . . 5
1211breq2d 4179 . . . 4
1312ralbidv 2683 . . 3
149, 13anbi12d 692 . 2
15 df-leop 23275 . 2
167, 14, 15brabg 4429 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1649   wcel 1721  wral 2663   class class class wbr 4167  cfv 5408  (class class class)co 6034  cc0 8937   cle 9068  chil 22342   csp 22345   chod 22363  cho 22373   cleo 22381 This theorem is referenced by:  leop  23546  leoprf2  23550 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-br 4168  df-opab 4222  df-iota 5372  df-fv 5416  df-ov 6037  df-leop 23275
 Copyright terms: Public domain W3C validator