Metamath Proof Explorer

Theorem pjin2i

Description: Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjin1.1 
|- G e. CH
pjin1.2 
|- H e. CH
Assertion pjin2i 
|- ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) <-> ( projh ` G ) = ( projh ` H ) )

Proof

Step Hyp Ref Expression
1 pjin1.1 
 |-  G e. CH
2 pjin1.2 
 |-  H e. CH
3 eqss 
 |-  ( G = H <-> ( G C_ H /\ H C_ G ) )
4 1 2 pjss2coi 
 |-  ( G C_ H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) )
5 eqcom 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) <-> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) )
6 4 5 bitri 
 |-  ( G C_ H <-> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) )
7 2 1 pjss2coi 
 |-  ( H C_ G <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` H ) )
8 eqcom 
 |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` H ) <-> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) )
9 7 8 bitri 
 |-  ( H C_ G <-> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) )
10 6 9 anbi12i 
 |-  ( ( G C_ H /\ H C_ G ) <-> ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) )
11 3 10 bitr2i 
 |-  ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) <-> G = H )
12 fveq2 
 |-  ( G = H -> ( projh ` G ) = ( projh ` H ) )
13 11 12 sylbi 
 |-  ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) -> ( projh ` G ) = ( projh ` H ) )
14 1 pjidmcoi 
 |-  ( ( projh ` G ) o. ( projh ` G ) ) = ( projh ` G )
15 coeq2 
 |-  ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` G ) o. ( projh ` G ) ) = ( ( projh ` G ) o. ( projh ` H ) ) )
16 14 15 eqtr3id 
 |-  ( ( projh ` G ) = ( projh ` H ) -> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) )
17 coeq2 
 |-  ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` H ) o. ( projh ` G ) ) = ( ( projh ` H ) o. ( projh ` H ) ) )
18 2 pjidmcoi 
 |-  ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H )
19 17 18 eqtr2di 
 |-  ( ( projh ` G ) = ( projh ` H ) -> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) )
20 16 19 jca 
 |-  ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) )
21 13 20 impbii 
 |-  ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) <-> ( projh ` G ) = ( projh ` H ) )