Theorem pj2cocli

Description: Closure of double composition of projections. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjadj2co.1	⊢ 𝐹 ∈ Cℋ
	pjadj2co.2	⊢ 𝐺 ∈ Cℋ
	pjadj2co.3	⊢ 𝐻 ∈ Cℋ
Assertion	pj2cocli	⊢ ( 𝐴 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		pjadj2co.1	⊢ 𝐹 ∈ Cℋ
2		pjadj2co.2	⊢ 𝐺 ∈ Cℋ
3		pjadj2co.3	⊢ 𝐻 ∈ Cℋ
4	1	pjfi	⊢ ( projℎ ‘ 𝐹 ) : ℋ ⟶ ℋ
5	2	pjfi	⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
6	3	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
7	4 5 6	ho2coi	⊢ ( 𝐴 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐹 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
8	3	pjhcli	⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )
9	2	pjhcli	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ )
10	1	pjcli	⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ → ( ( projℎ ‘ 𝐹 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ∈ 𝐹 )
11	8 9 10	3syl	⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐹 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ∈ 𝐹 )
12	7 11	eqeltrd	⊢ ( 𝐴 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐹 )