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ℎ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝐴 )