Metamath Proof Explorer

Theorem pjss2coi

Description: Subset relationship for projections. Theorem 4.5(i)<->(ii) of Beran p. 112. (Contributed by NM, 7-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjss2coi 
|- ( G C_ H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 1 2 pjcoi 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) )
4 3 adantl 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) )
5 2fveq3 
 |-  ( x = if ( x e. ~H , x , 0h ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = ( ( projh ` G ) ` ( ( projh ` H ) ` if ( x e. ~H , x , 0h ) ) ) )
6 fveq2 
 |-  ( x = if ( x e. ~H , x , 0h ) -> ( ( projh ` G ) ` x ) = ( ( projh ` G ) ` if ( x e. ~H , x , 0h ) ) )
7 5 6 eqeq12d 
 |-  ( x = if ( x e. ~H , x , 0h ) -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = ( ( projh ` G ) ` x ) <-> ( ( projh ` G ) ` ( ( projh ` H ) ` if ( x e. ~H , x , 0h ) ) ) = ( ( projh ` G ) ` if ( x e. ~H , x , 0h ) ) ) )
8 7 imbi2d 
 |-  ( x = if ( x e. ~H , x , 0h ) -> ( ( G C_ H -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = ( ( projh ` G ) ` x ) ) <-> ( G C_ H -> ( ( projh ` G ) ` ( ( projh ` H ) ` if ( x e. ~H , x , 0h ) ) ) = ( ( projh ` G ) ` if ( x e. ~H , x , 0h ) ) ) ) )
9 ifhvhv0 
 |-  if ( x e. ~H , x , 0h ) e. ~H
10 1 9 2 pjss2i 
 |-  ( G C_ H -> ( ( projh ` G ) ` ( ( projh ` H ) ` if ( x e. ~H , x , 0h ) ) ) = ( ( projh ` G ) ` if ( x e. ~H , x , 0h ) ) )
11 8 10 dedth 
 |-  ( x e. ~H -> ( G C_ H -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = ( ( projh ` G ) ` x ) ) )
12 11 impcom 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = ( ( projh ` G ) ` x ) )
13 4 12 eqtrd 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` x ) )
14 13 ralrimiva 
 |-  ( G C_ H -> A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` x ) )
15 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
16 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
17 15 16 hocofi 
 |-  ( ( projh ` G ) o. ( projh ` H ) ) : ~H --> ~H
18 17 15 hoeqi 
 |-  ( A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` x ) <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) )
19 14 18 sylib 
 |-  ( G C_ H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) )
20 fveq1 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) = ( ( projh ` G ) ` y ) )
21 20 oveq2d 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( projh ` G ) ` y ) ) )
22 21 ad2antlr 
 |-  ( ( ( x e. ~H /\ ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) ) /\ y e. ~H ) -> ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( projh ` G ) ` y ) ) )
23 2 1 pjadjcoi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) )
24 23 adantlr 
 |-  ( ( ( x e. ~H /\ ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) ) /\ y e. ~H ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) )
25 1 pjadji 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( projh ` G ) ` x ) .ih y ) = ( x .ih ( ( projh ` G ) ` y ) ) )
26 25 adantlr 
 |-  ( ( ( x e. ~H /\ ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) ) /\ y e. ~H ) -> ( ( ( projh ` G ) ` x ) .ih y ) = ( x .ih ( ( projh ` G ) ` y ) ) )
27 22 24 26 3eqtr4d 
 |-  ( ( ( x e. ~H /\ ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) ) /\ y e. ~H ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( ( ( projh ` G ) ` x ) .ih y ) )
28 27 exp31 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( y e. ~H -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( ( ( projh ` G ) ` x ) .ih y ) ) ) )
29 28 ralrimdv 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> A. y e. ~H ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( ( ( projh ` G ) ` x ) .ih y ) ) )
30 2 1 pjcohcli 
 |-  ( x e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) e. ~H )
31 1 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` G ) ` x ) e. ~H )
32 hial2eq 
 |-  ( ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) e. ~H /\ ( ( projh ` G ) ` x ) e. ~H ) -> ( A. y e. ~H ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( ( ( projh ` G ) ` x ) .ih y ) <-> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) ) )
33 30 31 32 syl2anc 
 |-  ( x e. ~H -> ( A. y e. ~H ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( ( ( projh ` G ) ` x ) .ih y ) <-> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) ) )
34 29 33 sylibd 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) ) )
35 34 com12 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( x e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) ) )
36 35 ralrimiv 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> A. x e. ~H ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) )
37 16 15 hocofi 
 |-  ( ( projh ` H ) o. ( projh ` G ) ) : ~H --> ~H
38 37 15 hoeqi 
 |-  ( A. x e. ~H ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )
39 36 38 sylib 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )
40 1 2 pjss1coi 
 |-  ( G C_ H <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )
41 39 40 sylibr 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) -> G C_ H )
42 19 41 impbii 
 |-  ( G C_ H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) )