Metamath Proof Explorer

Theorem trlcone

Description: If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 trlcone.b 
 |-  B = ( Base ` K )
2 trlcone.h 
 |-  H = ( LHyp ` K )
3 trlcone.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 trlcone.r 
 |-  R = ( ( trL ` K ) ` W )
5 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( R ` F ) =/= ( R ` G ) )
6 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( K e. HL /\ W e. H ) )
7 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> F e. T )
8 2 3 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
9 6 7 8 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> `' F e. T )
10 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> G e. T )
11 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
12 6 7 10 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( F o. G ) e. T )
13 eqid 
 |-  ( le ` K ) = ( le ` K )
14 eqid 
 |-  ( join ` K ) = ( join ` K )
15 13 14 2 3 4 trlco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ `' F e. T /\ ( F o. G ) e. T ) -> ( R ` ( `' F o. ( F o. G ) ) ) ( le ` K ) ( ( R ` `' F ) ( join ` K ) ( R ` ( F o. G ) ) ) )
16 6 9 12 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` ( `' F o. ( F o. G ) ) ) ( le ` K ) ( ( R ` `' F ) ( join ` K ) ( R ` ( F o. G ) ) ) )
17 coass 
 |-  ( ( `' F o. F ) o. G ) = ( `' F o. ( F o. G ) )
18 1 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B )
19 6 7 18 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> F : B -1-1-onto-> B )
20 f1ococnv1 
 |-  ( F : B -1-1-onto-> B -> ( `' F o. F ) = ( _I |` B ) )
21 19 20 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( `' F o. F ) = ( _I |` B ) )
22 21 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( `' F o. F ) o. G ) = ( ( _I |` B ) o. G ) )
23 1 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> G : B -1-1-onto-> B )
24 6 10 23 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> G : B -1-1-onto-> B )
25 f1of 
 |-  ( G : B -1-1-onto-> B -> G : B --> B )
26 fcoi2 
 |-  ( G : B --> B -> ( ( _I |` B ) o. G ) = G )
27 24 25 26 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( _I |` B ) o. G ) = G )
28 22 27 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( `' F o. F ) o. G ) = G )
29 17 28 syl5reqr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> G = ( `' F o. ( F o. G ) ) )
30 29 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` G ) = ( R ` ( `' F o. ( F o. G ) ) ) )
31 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> K e. HL )
32 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` F ) e. ( Atoms ` K ) )
33 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
34 14 33 hlatjidm 
 |-  ( ( K e. HL /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` F ) ( join ` K ) ( R ` F ) ) = ( R ` F ) )
35 31 32 34 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( R ` F ) ( join ` K ) ( R ` F ) ) = ( R ` F ) )
36 2 3 4 trlcnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )
37 6 7 36 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` `' F ) = ( R ` F ) )
38 37 eqcomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` F ) = ( R ` `' F ) )
39 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` F ) = ( R ` ( F o. G ) ) )
40 38 39 oveq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( R ` F ) ( join ` K ) ( R ` F ) ) = ( ( R ` `' F ) ( join ` K ) ( R ` ( F o. G ) ) ) )
41 35 40 eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` F ) = ( ( R ` `' F ) ( join ` K ) ( R ` ( F o. G ) ) ) )
42 16 30 41 3brtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` G ) ( le ` K ) ( R ` F ) )
43 hlatl 
 |-  ( K e. HL -> K e. AtLat )
44 31 43 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> K e. AtLat )
45 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> G =/= ( _I |` B ) )
46 1 33 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. ( Atoms ` K ) )
47 6 10 45 46 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` G ) e. ( Atoms ` K ) )
48 13 33 atcmp 
 |-  ( ( K e. AtLat /\ ( R ` G ) e. ( Atoms ` K ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` G ) ( le ` K ) ( R ` F ) <-> ( R ` G ) = ( R ` F ) ) )
49 44 47 32 48 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( ( R ` G ) ( le ` K ) ( R ` F ) <-> ( R ` G ) = ( R ` F ) ) )
50 42 49 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` G ) = ( R ` F ) )
51 50 eqcomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) /\ ( R ` F ) = ( R ` ( F o. G ) ) ) -> ( R ` F ) = ( R ` G ) )
52 51 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` F ) = ( R ` ( F o. G ) ) -> ( R ` F ) = ( R ` G ) ) )
53 52 necon3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` F ) =/= ( R ` G ) -> ( R ` F ) =/= ( R ` ( F o. G ) ) ) )
54 5 53 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( R ` F ) =/= ( R ` ( F o. G ) ) )
55 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> G =/= ( _I |` B ) )
56 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( K e. HL /\ W e. H ) )
57 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> G e. T )
58 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
59 1 58 2 3 4 trlid0b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( G = ( _I |` B ) <-> ( R ` G ) = ( 0. ` K ) ) )
60 56 57 59 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( G = ( _I |` B ) <-> ( R ` G ) = ( 0. ` K ) ) )
61 60 necon3bid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( G =/= ( _I |` B ) <-> ( R ` G ) =/= ( 0. ` K ) ) )
62 55 61 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` G ) =/= ( 0. ` K ) )
63 62 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( 0. ` K ) =/= ( R ` G ) )
64 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` F ) = ( 0. ` K ) )
65 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> F e. T )
66 1 58 2 3 4 trlid0b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F = ( _I |` B ) <-> ( R ` F ) = ( 0. ` K ) ) )
67 56 65 66 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( F = ( _I |` B ) <-> ( R ` F ) = ( 0. ` K ) ) )
68 64 67 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> F = ( _I |` B ) )
69 68 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( F o. G ) = ( ( _I |` B ) o. G ) )
70 56 57 23 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> G : B -1-1-onto-> B )
71 70 25 26 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( ( _I |` B ) o. G ) = G )
72 69 71 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( F o. G ) = G )
73 72 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` ( F o. G ) ) = ( R ` G ) )
74 63 64 73 3netr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` F ) =/= ( R ` ( F o. G ) ) )
75 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) -> ( K e. HL /\ W e. H ) )
76 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) -> F e. T )
77 58 33 2 3 4 trlator0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. ( Atoms ` K ) \/ ( R ` F ) = ( 0. ` K ) ) )
78 75 76 77 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) -> ( ( R ` F ) e. ( Atoms ` K ) \/ ( R ` F ) = ( 0. ` K ) ) )
79 54 74 78 mpjaodan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) -> ( R ` F ) =/= ( R ` ( F o. G ) ) )