Metamath Proof Explorer

Theorem pjss2i

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

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjsslem.1 
|- G e. CH
Assertion pjss2i 
|- ( H C_ G -> ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` A ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjsslem.1 
 |-  G e. CH
4 1 choccli 
 |-  ( _|_ ` H ) e. CH
5 4 2 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H )
6 1 3 chsscon3i 
 |-  ( H C_ G <-> ( _|_ ` G ) C_ ( _|_ ` H ) )
7 3 choccli 
 |-  ( _|_ ` G ) e. CH
8 7 2 pjclii 
 |-  ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G )
9 ssel 
 |-  ( ( _|_ ` G ) C_ ( _|_ ` H ) -> ( ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) )
10 8 9 mpi 
 |-  ( ( _|_ ` G ) C_ ( _|_ ` H ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) )
11 6 10 sylbi 
 |-  ( H C_ G -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) )
12 4 chshii 
 |-  ( _|_ ` H ) e. SH
13 shsubcl 
 |-  ( ( ( _|_ ` H ) e. SH /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
14 12 13 mp3an1 
 |-  ( ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
15 5 11 14 sylancr 
 |-  ( H C_ G -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
16 1 2 3 pjsslem 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) )
17 16 eleq1i 
 |-  ( ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) <-> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) )
18 3 2 pjhclii 
 |-  ( ( projh ` G ) ` A ) e. ~H
19 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
20 18 19 hvsubcli 
 |-  ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ~H
21 1 20 pjoc2i 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) <-> ( ( projh ` H ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = 0h )
22 17 21 bitri 
 |-  ( ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) <-> ( ( projh ` H ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = 0h )
23 1 18 19 pjsubii 
 |-  ( ( projh ` H ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) )
24 23 eqeq1i 
 |-  ( ( ( projh ` H ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = 0h <-> ( ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) ) = 0h )
25 1 18 pjhclii 
 |-  ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) e. ~H
26 1 19 pjhclii 
 |-  ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) e. ~H
27 25 26 hvsubeq0i 
 |-  ( ( ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) ) = 0h <-> ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) )
28 24 27 bitri 
 |-  ( ( ( projh ` H ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = 0h <-> ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) )
29 1 2 pjidmi 
 |-  ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A )
30 29 eqeq2i 
 |-  ( ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` ( ( projh ` H ) ` A ) ) <-> ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` A ) )
31 22 28 30 3bitrri 
 |-  ( ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` A ) <-> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
32 15 31 sylibr 
 |-  ( H C_ G -> ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` H ) ` A ) )