Metamath Proof Explorer


Theorem pjcoi

Description: Composition of projections. (Contributed by NM, 16-Aug-2000) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjco.1 𝐺C
2 pjco.2 𝐻C
3 1 pjfi ( proj𝐺 ) : ℋ ⟶ ℋ
4 2 pjfi ( proj𝐻 ) : ℋ ⟶ ℋ
5 3 4 hocoi ( 𝐴 ∈ ℋ → ( ( ( proj𝐺 ) ∘ ( proj𝐻 ) ) ‘ 𝐴 ) = ( ( proj𝐺 ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) )