Metamath Proof Explorer

Theorem pjclem3

Description: Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 
|- G e. CH
pjclem1.2 
|- H e. CH
Assertion pjclem3 
|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( ( projh ` ( _|_ ` H ) ) o. ( projh ` G ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 
 |-  G e. CH
2 pjclem1.2 
 |-  H e. CH
3 df-iop 
 |-  Iop = ( projh ` ~H )
4 3 coeq2i 
 |-  ( ( projh ` G ) o. Iop ) = ( ( projh ` G ) o. ( projh ` ~H ) )
5 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
6 5 hoid1i 
 |-  ( ( projh ` G ) o. Iop ) = ( projh ` G )
7 4 6 eqtr3i 
 |-  ( ( projh ` G ) o. ( projh ` ~H ) ) = ( projh ` G )
8 5 hoid1ri 
 |-  ( Iop o. ( projh ` G ) ) = ( projh ` G )
9 3 coeq1i 
 |-  ( Iop o. ( projh ` G ) ) = ( ( projh ` ~H ) o. ( projh ` G ) )
10 7 8 9 3eqtr2i 
 |-  ( ( projh ` G ) o. ( projh ` ~H ) ) = ( ( projh ` ~H ) o. ( projh ` G ) )
11 10 oveq1i 
 |-  ( ( ( projh ` G ) o. ( projh ` ~H ) ) -op ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( ( projh ` ~H ) o. ( projh ` G ) ) -op ( ( projh ` G ) o. ( projh ` H ) ) )
12 oveq2 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( projh ` ~H ) o. ( projh ` G ) ) -op ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( ( projh ` ~H ) o. ( projh ` G ) ) -op ( ( projh ` H ) o. ( projh ` G ) ) ) )
13 11 12 syl5eq 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( projh ` G ) o. ( projh ` ~H ) ) -op ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( ( projh ` ~H ) o. ( projh ` G ) ) -op ( ( projh ` H ) o. ( projh ` G ) ) ) )
14 helch 
 |-  ~H e. CH
15 14 pjfi 
 |-  ( projh ` ~H ) : ~H --> ~H
16 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
17 1 15 16 pjddii 
 |-  ( ( projh ` G ) o. ( ( projh ` ~H ) -op ( projh ` H ) ) ) = ( ( ( projh ` G ) o. ( projh ` ~H ) ) -op ( ( projh ` G ) o. ( projh ` H ) ) )
18 15 16 5 hocsubdiri 
 |-  ( ( ( projh ` ~H ) -op ( projh ` H ) ) o. ( projh ` G ) ) = ( ( ( projh ` ~H ) o. ( projh ` G ) ) -op ( ( projh ` H ) o. ( projh ` G ) ) )
19 13 17 18 3eqtr4g 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( ( projh ` ~H ) -op ( projh ` H ) ) ) = ( ( ( projh ` ~H ) -op ( projh ` H ) ) o. ( projh ` G ) ) )
20 2 pjoci 
 |-  ( ( projh ` ~H ) -op ( projh ` H ) ) = ( projh ` ( _|_ ` H ) )
21 20 coeq2i 
 |-  ( ( projh ` G ) o. ( ( projh ` ~H ) -op ( projh ` H ) ) ) = ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) )
22 20 coeq1i 
 |-  ( ( ( projh ` ~H ) -op ( projh ` H ) ) o. ( projh ` G ) ) = ( ( projh ` ( _|_ ` H ) ) o. ( projh ` G ) )
23 19 21 22 3eqtr3g 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( ( projh ` ( _|_ ` H ) ) o. ( projh ` G ) ) )