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 GC
pjco.2 HC
Assertion pjordi x0projH-opprojGxihxprojGprojH

Proof

Step Hyp Ref Expression
1 pjco.1 GC
2 pjco.2 HC
3 1 2 pjssposi x0projH-opprojGxihxGH
4 1 pjfoi projG:ontoG
5 foima projG:ontoGprojG=G
6 4 5 ax-mp projG=G
7 2 pjfoi projH:ontoH
8 foima projH:ontoHprojH=H
9 7 8 ax-mp projH=H
10 6 9 sseq12i projGprojHGH
11 3 10 bitr4i x0projH-opprojGxihxprojGprojH