Theorem trlcocnvat

Description: Commonly used special case of trlcoat . (Contributed by NM, 1-Jul-2013)

	Ref	Expression
Hypotheses	trlcoat.a	|- A = ( Atoms ` K )
	trlcoat.h	|- H = ( LHyp ` K )
	trlcoat.t	|- T = ( ( LTrn ` K ) ` W )
	trlcoat.r	|- R = ( ( trL ` K ) ` W )
Assertion	trlcocnvat	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. `' G ) ) e. A )

Proof

Step	Hyp	Ref	Expression
1		trlcoat.a	|- A = ( Atoms ` K )
2		trlcoat.h	|- H = ( LHyp ` K )
3		trlcoat.t	|- T = ( ( LTrn ` K ) ` W )
4		trlcoat.r	|- R = ( ( trL ` K ) ` W )
5		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( K e. HL /\ W e. H ) )
6		simp2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> F e. T )
7		simp2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> G e. T )
8	2 3	ltrncnv	|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
9	5 7 8	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> `' G e. T )
10		simp3	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` F ) =/= ( R ` G ) )
11	2 3 4	trlcnv	|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` `' G ) = ( R ` G ) )
12	5 7 11	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` `' G ) = ( R ` G ) )
13	10 12	neeqtrrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` F ) =/= ( R ` `' G ) )
14	1 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. A )
15	5 6 9 13 14	syl121anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. `' G ) ) e. A )