Metamath Proof Explorer

Theorem pj3i

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

		Ref	Expression
	Hypotheses	pjadj2co.1	\|- F e. CH
		pjadj2co.2	\|- G e. CH
		pjadj2co.3	\|- 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
1		pjadj2co.1	\|- F e. CH
2		pjadj2co.2	\|- G e. CH
3		pjadj2co.3	\|- 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 ) ) )