# 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 𝐺C
pjclem1.2 𝐻C
Assertion pjclem4a ( 𝐴 ∈ ( 𝐺𝐻 ) → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = 𝐴 )

### Proof

Step Hyp Ref Expression
1 pjclem1.1 𝐺C
2 pjclem1.2 𝐻C
3 elin ( 𝐴 ∈ ( 𝐺𝐻 ) ↔ ( 𝐴𝐺𝐴𝐻 ) )
4 2 cheli ( 𝐴𝐻𝐴 ∈ ℋ )
5 4 adantl ( ( 𝐴𝐺𝐴𝐻 ) → 𝐴 ∈ ℋ )
6 1 2 pjcoi ( 𝐴 ∈ ℋ → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) )
7 5 6 syl ( ( 𝐴𝐺𝐴𝐻 ) → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) )
8 pjid ( ( 𝐻C𝐴𝐻 ) → ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 )
9 2 8 mpan ( 𝐴𝐻 → ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 )
10 eleq1 ( ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 → ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺𝐴𝐺 ) )
11 pjid ( ( 𝐺C ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 ) → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj𝐻 ) ‘ 𝐴 ) )
12 1 11 mpan ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj𝐻 ) ‘ 𝐴 ) )
13 10 12 syl6bir ( ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 → ( 𝐴𝐺 → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj𝐻 ) ‘ 𝐴 ) ) )
14 eqeq2 ( ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 → ( ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj𝐻 ) ‘ 𝐴 ) ↔ ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) )
15 13 14 sylibd ( ( ( proj𝐻 ) ‘ 𝐴 ) = 𝐴 → ( 𝐴𝐺 → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) )
16 9 15 syl ( 𝐴𝐻 → ( 𝐴𝐺 → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) )
17 16 impcom ( ( 𝐴𝐺𝐴𝐻 ) → ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 𝐴 )
18 7 17 eqtrd ( ( 𝐴𝐺𝐴𝐻 ) → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = 𝐴 )
19 3 18 sylbi ( 𝐴 ∈ ( 𝐺𝐻 ) → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = 𝐴 )