Metamath Proof Explorer

Theorem pj2cocli

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

Ref Expression
Hypotheses pjadj2co.1 ⊢F∈Cℋ
pjadj2co.2 ⊢G∈Cℋ
pjadj2co.3 ⊢H∈Cℋ
Assertion pj2cocli ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A∈F

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢F∈Cℋ
2 pjadj2co.2 ⊢G∈Cℋ
3 pjadj2co.3 ⊢H∈Cℋ
4 1 pjfi ⊢projℎ⁡F:ℋ⟶ℋ
5 2 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
6 3 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
7 4 5 6 ho2coi ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡F⁡projℎ⁡G⁡projℎ⁡H⁡A
8 3 pjhcli ⊢A∈ℋ→projℎ⁡H⁡A∈ℋ
9 2 pjhcli ⊢projℎ⁡H⁡A∈ℋ→projℎ⁡G⁡projℎ⁡H⁡A∈ℋ
10 1 pjcli ⊢projℎ⁡G⁡projℎ⁡H⁡A∈ℋ→projℎ⁡F⁡projℎ⁡G⁡projℎ⁡H⁡A∈F
11 8 9 10 3syl ⊢A∈ℋ→projℎ⁡F⁡projℎ⁡G⁡projℎ⁡H⁡A∈F
12 7 11 eqeltrd ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A∈F