# Metamath Proof Explorer

## Theorem pj3i

Description: Projection triplet theorem. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

Ref Expression
`|- F e. CH`
`|- G e. CH`
`|- H e. CH`
Assertion pj3i
`|- ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )`

### Proof

Step Hyp Ref Expression
` |-  F e. CH`
` |-  G e. CH`
` |-  H e. CH`
4 coass
` |-  ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) = ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) )`
5 eqeq1
` |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) <-> ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) = ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) ) )`
6 4 5 mpbiri
` |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) )`
7 6 rneqd
` |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ran ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) )`
8 rncoss
` |-  ran ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) C_ ran ( projh ` G )`
9 2 pjrni
` |-  ran ( projh ` G ) = G`
10 8 9 sseqtri
` |-  ran ( ( projh ` G ) o. ( ( projh ` F ) o. ( projh ` H ) ) ) C_ G`
11 7 10 eqsstrdi
` |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G )`
12 1 2 3 pj3si
` |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )`
13 11 12 sylan2
` |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )`