Metamath Proof Explorer

Theorem pjsslem

Description: Lemma for subset relationships of projections. (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 pjsslem 
|- ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( ( ( projh ` G ) ` A ) -h ( ( 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 pjo 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) )
5 1 2 4 mp2an 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) )
6 pjo 
 |-  ( ( G e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
7 3 2 6 mp2an 
 |-  ( ( projh ` ( _|_ ` G ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` G ) ` A ) )
8 5 7 oveq12i 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) -h ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
9 helch 
 |-  ~H e. CH
10 9 2 pjclii 
 |-  ( ( projh ` ~H ) ` A ) e. ~H
11 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
12 3 2 pjhclii 
 |-  ( ( projh ` G ) ` A ) e. ~H
13 10 11 10 12 hvsubsub4i 
 |-  ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) -h ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` G ) ` A ) ) ) = ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) -h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
14 hvsubid 
 |-  ( ( ( projh ` ~H ) ` A ) e. ~H -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h )
15 10 14 ax-mp 
 |-  ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h
16 15 oveq1i 
 |-  ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) -h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) ) = ( 0h -h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
17 8 13 16 3eqtri 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( 0h -h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
18 11 12 hvsubcli 
 |-  ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) e. ~H
19 18 hv2negi 
 |-  ( 0h -h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) ) = ( -u 1 .h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) )
20 11 12 hvnegdii 
 |-  ( -u 1 .h ( ( ( projh ` H ) ` A ) -h ( ( projh ` G ) ` A ) ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) )
21 17 19 20 3eqtri 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) )