Theorem trlconid

Description: The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013)

	Ref	Expression
Hypotheses	trlconid.b	|- B = ( Base ` K )
	trlconid.h	|- H = ( LHyp ` K )
	trlconid.t	|- T = ( ( LTrn ` K ) ` W )
	trlconid.r	|- R = ( ( trL ` K ) ` W )
Assertion	trlconid	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) =/= ( _I |` B ) )

Proof

Step	Hyp	Ref	Expression
1		trlconid.b	|- B = ( Base ` K )
2		trlconid.h	|- H = ( LHyp ` K )
3		trlconid.t	|- T = ( ( LTrn ` K ) ` W )
4		trlconid.r	|- R = ( ( trL ` K ) ` W )
5		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
6	5 2 3 4	trlcoat	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. G ) ) e. ( Atoms ` K ) )
7		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( K e. HL /\ W e. H ) )
8		simp2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> F e. T )
9		simp2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> G e. T )
10	2 3	ltrnco	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
11	7 8 9 10	syl3anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) e. T )
12	1 5 2 3 4	trlnidatb	|- ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T ) -> ( ( F o. G ) =/= ( _I |` B ) <-> ( R ` ( F o. G ) ) e. ( Atoms ` K ) ) )
13	7 11 12	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( ( F o. G ) =/= ( _I |` B ) <-> ( R ` ( F o. G ) ) e. ( Atoms ` K ) ) )
14	6 13	mpbird	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) =/= ( _I |` B ) )