Metamath Proof Explorer


Theorem pjordi

Description: The definition of projector ordering in Halmos p. 42 is equivalent to the definition of projector ordering in Beran p. 110. (We will usually express projector ordering with the even simpler equivalent G C_ H ; see pjssposi ). (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1
|- G e. CH
pjco.2
|- H e. CH
Assertion pjordi
|- ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> ( ( projh ` G ) " ~H ) C_ ( ( projh ` H ) " ~H ) )

Proof

Step Hyp Ref Expression
1 pjco.1
 |-  G e. CH
2 pjco.2
 |-  H e. CH
3 1 2 pjssposi
 |-  ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> G C_ H )
4 1 pjfoi
 |-  ( projh ` G ) : ~H -onto-> G
5 foima
 |-  ( ( projh ` G ) : ~H -onto-> G -> ( ( projh ` G ) " ~H ) = G )
6 4 5 ax-mp
 |-  ( ( projh ` G ) " ~H ) = G
7 2 pjfoi
 |-  ( projh ` H ) : ~H -onto-> H
8 foima
 |-  ( ( projh ` H ) : ~H -onto-> H -> ( ( projh ` H ) " ~H ) = H )
9 7 8 ax-mp
 |-  ( ( projh ` H ) " ~H ) = H
10 6 9 sseq12i
 |-  ( ( ( projh ` G ) " ~H ) C_ ( ( projh ` H ) " ~H ) <-> G C_ H )
11 3 10 bitr4i
 |-  ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> ( ( projh ` G ) " ~H ) C_ ( ( projh ` H ) " ~H ) )