Theorem pjcocli

Description: Closure of composition of projections. (Contributed by NM, 29-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	⊢ 𝐺 ∈ Cℋ
	pjco.2	⊢ 𝐻 ∈ Cℋ
Assertion	pjcocli	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		pjco.1	⊢ 𝐺 ∈ Cℋ
2		pjco.2	⊢ 𝐻 ∈ Cℋ
3	1 2	pjcoi	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
4	2	pjhcli	⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )
5	1	pjcli	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 )
6	4 5	syl	⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 )
7	3 6	eqeltrd	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐺 )