# Metamath Proof Explorer

## Theorem pjclem4a

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

Ref Expression
Hypotheses pjclem1.1
`|- G e. CH`
pjclem1.2
`|- H e. CH`
Assertion pjclem4a
`|- ( A e. ( G i^i H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )`

### Proof

Step Hyp Ref Expression
1 pjclem1.1
` |-  G e. CH`
2 pjclem1.2
` |-  H e. CH`
3 elin
` |-  ( A e. ( G i^i H ) <-> ( A e. G /\ A e. H ) )`
4 2 cheli
` |-  ( A e. H -> A e. ~H )`
` |-  ( ( A e. G /\ A e. H ) -> A e. ~H )`
6 1 2 pjcoi
` |-  ( A e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) )`
7 5 6 syl
` |-  ( ( A e. G /\ A e. H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) )`
8 pjid
` |-  ( ( H e. CH /\ A e. H ) -> ( ( projh ` H ) ` A ) = A )`
9 2 8 mpan
` |-  ( A e. H -> ( ( projh ` H ) ` A ) = A )`
10 eleq1
` |-  ( ( ( projh ` H ) ` A ) = A -> ( ( ( projh ` H ) ` A ) e. G <-> A e. G ) )`
11 pjid
` |-  ( ( G e. CH /\ ( ( projh ` H ) ` A ) e. G ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) )`
12 1 11 mpan
` |-  ( ( ( projh ` H ) ` A ) e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) )`
13 10 12 syl6bir
` |-  ( ( ( projh ` H ) ` A ) = A -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) ) )`
14 eqeq2
` |-  ( ( ( projh ` H ) ` A ) = A -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) <-> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )`
15 13 14 sylibd
` |-  ( ( ( projh ` H ) ` A ) = A -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )`
16 9 15 syl
` |-  ( A e. H -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )`
17 16 impcom
` |-  ( ( A e. G /\ A e. H ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A )`
18 7 17 eqtrd
` |-  ( ( A e. G /\ A e. H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )`
19 3 18 sylbi
` |-  ( A e. ( G i^i H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )`