Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trljco Structured version   Unicode version

Theorem trljco 34693
Description: Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.)
Hypotheses
Ref Expression
trljco.j  |-  .\/  =  ( join `  K )
trljco.h  |-  H  =  ( LHyp `  K
)
trljco.t  |-  T  =  ( ( LTrn `  K
) `  W )
trljco.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
trljco  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  G ) ) )

Proof of Theorem trljco
StepHypRef Expression
1 coeq1 5098 . . . . 5  |-  ( F  =  (  _I  |`  ( Base `  K ) )  ->  ( F  o.  G )  =  ( (  _I  |`  ( Base `  K ) )  o.  G ) )
2 eqid 2451 . . . . . . . 8  |-  ( Base `  K )  =  (
Base `  K )
3 trljco.h . . . . . . . 8  |-  H  =  ( LHyp `  K
)
4 trljco.t . . . . . . . 8  |-  T  =  ( ( LTrn `  K
) `  W )
52, 3, 4ltrn1o 34077 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  G :
( Base `  K ) -1-1-onto-> ( Base `  K ) )
653adant2 1007 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  G :
( Base `  K ) -1-1-onto-> ( Base `  K ) )
7 f1of 5742 . . . . . 6  |-  ( G : ( Base `  K
)
-1-1-onto-> ( Base `  K )  ->  G : ( Base `  K ) --> ( Base `  K ) )
8 fcoi2 5687 . . . . . 6  |-  ( G : ( Base `  K
) --> ( Base `  K
)  ->  ( (  _I  |`  ( Base `  K
) )  o.  G
)  =  G )
96, 7, 83syl 20 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( (  _I  |`  ( Base `  K
) )  o.  G
)  =  G )
101, 9sylan9eqr 2514 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  F  =  (  _I  |`  ( Base `  K ) ) )  ->  ( F  o.  G )  =  G )
1110fveq2d 5796 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  F  =  (  _I  |`  ( Base `  K ) ) )  ->  ( R `  ( F  o.  G
) )  =  ( R `  G ) )
1211oveq2d 6209 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  F  =  (  _I  |`  ( Base `  K ) ) )  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  G ) ) )
13 simp1l 1012 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  K  e.  HL )
14 hllat 33317 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  Lat )
1513, 14syl 16 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  K  e.  Lat )
16 trljco.r . . . . . . . 8  |-  R  =  ( ( trL `  K
) `  W )
172, 3, 4, 16trlcl 34117 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  e.  (
Base `  K )
)
18173adant3 1008 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  F )  e.  (
Base `  K )
)
19 trljco.j . . . . . . 7  |-  .\/  =  ( join `  K )
202, 19latjidm 15355 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( R `  F )  e.  ( Base `  K
) )  ->  (
( R `  F
)  .\/  ( R `  F ) )  =  ( R `  F
) )
2115, 18, 20syl2anc 661 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  F
) )  =  ( R `  F ) )
22 hlol 33315 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  OL )
2313, 22syl 16 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  K  e.  OL )
24 eqid 2451 . . . . . . 7  |-  ( 0.
`  K )  =  ( 0. `  K
)
252, 19, 24olj01 33179 . . . . . 6  |-  ( ( K  e.  OL  /\  ( R `  F )  e.  ( Base `  K
) )  ->  (
( R `  F
)  .\/  ( 0. `  K ) )  =  ( R `  F
) )
2623, 18, 25syl2anc 661 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( 0. `  K
) )  =  ( R `  F ) )
2721, 26eqtr4d 2495 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  F
) )  =  ( ( R `  F
)  .\/  ( 0. `  K ) ) )
2827adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( ( R `  F )  .\/  ( R `  F
) )  =  ( ( R `  F
)  .\/  ( 0. `  K ) ) )
29 coeq2 5099 . . . . . 6  |-  ( G  =  (  _I  |`  ( Base `  K ) )  ->  ( F  o.  G )  =  ( F  o.  (  _I  |`  ( Base `  K
) ) ) )
302, 3, 4ltrn1o 34077 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  F :
( Base `  K ) -1-1-onto-> ( Base `  K ) )
31303adant3 1008 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  F :
( Base `  K ) -1-1-onto-> ( Base `  K ) )
32 f1of 5742 . . . . . . 7  |-  ( F : ( Base `  K
)
-1-1-onto-> ( Base `  K )  ->  F : ( Base `  K ) --> ( Base `  K ) )
33 fcoi1 5686 . . . . . . 7  |-  ( F : ( Base `  K
) --> ( Base `  K
)  ->  ( F  o.  (  _I  |`  ( Base `  K ) ) )  =  F )
3431, 32, 333syl 20 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( F  o.  (  _I  |`  ( Base `  K ) ) )  =  F )
3529, 34sylan9eqr 2514 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( F  o.  G )  =  F )
3635fveq2d 5796 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( R `  ( F  o.  G
) )  =  ( R `  F ) )
3736oveq2d 6209 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  F ) ) )
382, 24, 3, 4, 16trlid0b 34131 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( G  =  (  _I  |`  ( Base `  K ) )  <-> 
( R `  G
)  =  ( 0.
`  K ) ) )
39383adant2 1007 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( G  =  (  _I  |`  ( Base `  K ) )  <-> 
( R `  G
)  =  ( 0.
`  K ) ) )
4039biimpa 484 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( R `  G )  =  ( 0. `  K ) )
4140oveq2d 6209 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( ( R `  F )  .\/  ( R `  G
) )  =  ( ( R `  F
)  .\/  ( 0. `  K ) ) )
4228, 37, 413eqtr4d 2502 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  G  =  (  _I  |`  ( Base `  K ) ) )  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  G ) ) )
43 eqid 2451 . . 3  |-  ( le
`  K )  =  ( le `  K
)
4415adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  ->  K  e.  Lat )
45 simp1 988 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( K  e.  HL  /\  W  e.  H ) )
463, 4ltrnco 34672 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( F  o.  G )  e.  T
)
472, 3, 4, 16trlcl 34117 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  o.  G )  e.  T
)  ->  ( R `  ( F  o.  G
) )  e.  (
Base `  K )
)
4845, 46, 47syl2anc 661 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  ( F  o.  G
) )  e.  (
Base `  K )
)
492, 19latjcl 15332 . . . . 5  |-  ( ( K  e.  Lat  /\  ( R `  F )  e.  ( Base `  K
)  /\  ( R `  ( F  o.  G
) )  e.  (
Base `  K )
)  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  e.  (
Base `  K )
)
5015, 18, 48, 49syl3anc 1219 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  e.  (
Base `  K )
)
5150adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) )  e.  ( Base `  K
) )
522, 3, 4, 16trlcl 34117 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( R `  G )  e.  (
Base `  K )
)
53523adant2 1007 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  G )  e.  (
Base `  K )
)
542, 19latjcl 15332 . . . . 5  |-  ( ( K  e.  Lat  /\  ( R `  F )  e.  ( Base `  K
)  /\  ( R `  G )  e.  (
Base `  K )
)  ->  ( ( R `  F )  .\/  ( R `  G
) )  e.  (
Base `  K )
)
5515, 18, 53, 54syl3anc 1219 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  G
) )  e.  (
Base `  K )
)
5655adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  G )
)  e.  ( Base `  K ) )
572, 43, 19latlej1 15341 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( R `  F )  e.  ( Base `  K
)  /\  ( R `  G )  e.  (
Base `  K )
)  ->  ( R `  F ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) )
5815, 18, 53, 57syl3anc 1219 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  F ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) )
5943, 19, 3, 4, 16trlco 34680 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  ( F  o.  G
) ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) )
602, 43, 19latjle12 15343 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( R `  F )  e.  (
Base `  K )  /\  ( R `  ( F  o.  G )
)  e.  ( Base `  K )  /\  (
( R `  F
)  .\/  ( R `  G ) )  e.  ( Base `  K
) ) )  -> 
( ( ( R `
 F ) ( le `  K ) ( ( R `  F )  .\/  ( R `  G )
)  /\  ( R `  ( F  o.  G
) ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) )  <-> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) ) ( le `  K
) ( ( R `
 F )  .\/  ( R `  G ) ) ) )
6115, 18, 48, 55, 60syl13anc 1221 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( (
( R `  F
) ( le `  K ) ( ( R `  F ) 
.\/  ( R `  G ) )  /\  ( R `  ( F  o.  G ) ) ( le `  K
) ( ( R `
 F )  .\/  ( R `  G ) ) )  <->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) ) )
6258, 59, 61mpbi2and 912 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  G ) ) )
6362adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) ) ( le `  K
) ( ( R `
 F )  .\/  ( R `  G ) ) )
64 simpr 461 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( R `  F
)  =  ( R `
 G ) )
6564oveq2d 6209 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  F )
)  =  ( ( R `  F ) 
.\/  ( R `  G ) ) )
662, 43, 19latlej1 15341 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( R `  F )  e.  ( Base `  K
)  /\  ( R `  ( F  o.  G
) )  e.  (
Base `  K )
)  ->  ( R `  F ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  ( F  o.  G
) ) ) )
6715, 18, 48, 66syl3anc 1219 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( R `  F ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  ( F  o.  G
) ) ) )
6821, 67eqbrtrd 4413 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  F
) ) ( le
`  K ) ( ( R `  F
)  .\/  ( R `  ( F  o.  G
) ) ) )
6968adantr 465 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  F )
) ( le `  K ) ( ( R `  F ) 
.\/  ( R `  ( F  o.  G
) ) ) )
7065, 69eqbrtrrd 4415 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  G )
) ( le `  K ) ( ( R `  F ) 
.\/  ( R `  ( F  o.  G
) ) ) )
712, 43, 44, 51, 56, 63, 70latasymd 15338 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =  ( R `  G ) )  -> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) )  =  ( ( R `
 F )  .\/  ( R `  G ) ) )
7262adantr 465 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) ) ( le `  K
) ( ( R `
 F )  .\/  ( R `  G ) ) )
73 simpl1l 1039 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  ->  K  e.  HL )
74 simpl1 991 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
75 simpl2 992 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  ->  F  e.  T )
76 simpr1 994 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  ->  F  =/=  (  _I  |`  ( Base `  K ) ) )
77 eqid 2451 . . . . . 6  |-  ( Atoms `  K )  =  (
Atoms `  K )
782, 77, 3, 4, 16trlnidat 34126 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  F  =/=  (  _I  |`  ( Base `  K
) ) )  -> 
( R `  F
)  e.  ( Atoms `  K ) )
7974, 75, 76, 78syl3anc 1219 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( R `  F
)  e.  ( Atoms `  K ) )
80 simpl3 993 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  ->  G  e.  T )
8175, 80jca 532 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( F  e.  T  /\  G  e.  T
) )
82 simpr3 996 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( R `  F
)  =/=  ( R `
 G ) )
8377, 3, 4, 16trlcoat 34676 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( R `  F )  =/=  ( R `  G
) )  ->  ( R `  ( F  o.  G ) )  e.  ( Atoms `  K )
)
8474, 81, 82, 83syl3anc 1219 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( R `  ( F  o.  G )
)  e.  ( Atoms `  K ) )
85 simpr2 995 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  ->  G  =/=  (  _I  |`  ( Base `  K ) ) )
862, 3, 4, 16trlcone 34681 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  (
( R `  F
)  =/=  ( R `
 G )  /\  G  =/=  (  _I  |`  ( Base `  K ) ) ) )  ->  ( R `  F )  =/=  ( R `  ( F  o.  G )
) )
8774, 81, 82, 85, 86syl112anc 1223 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( R `  F
)  =/=  ( R `
 ( F  o.  G ) ) )
882, 77, 3, 4, 16trlnidat 34126 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  G  =/=  (  _I  |`  ( Base `  K
) ) )  -> 
( R `  G
)  e.  ( Atoms `  K ) )
8974, 80, 85, 88syl3anc 1219 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( R `  G
)  e.  ( Atoms `  K ) )
9043, 19, 77ps-1 33430 . . . 4  |-  ( ( K  e.  HL  /\  ( ( R `  F )  e.  (
Atoms `  K )  /\  ( R `  ( F  o.  G ) )  e.  ( Atoms `  K
)  /\  ( R `  F )  =/=  ( R `  ( F  o.  G ) ) )  /\  ( ( R `
 F )  e.  ( Atoms `  K )  /\  ( R `  G
)  e.  ( Atoms `  K ) ) )  ->  ( ( ( R `  F ) 
.\/  ( R `  ( F  o.  G
) ) ) ( le `  K ) ( ( R `  F )  .\/  ( R `  G )
)  <->  ( ( R `
 F )  .\/  ( R `  ( F  o.  G ) ) )  =  ( ( R `  F ) 
.\/  ( R `  G ) ) ) )
9173, 79, 84, 87, 79, 89, 90syl132anc 1237 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( ( ( R `
 F )  .\/  ( R `  ( F  o.  G ) ) ) ( le `  K ) ( ( R `  F ) 
.\/  ( R `  G ) )  <->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  G ) ) ) )
9272, 91mpbid 210 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( F  =/=  (  _I  |`  ( Base `  K ) )  /\  G  =/=  (  _I  |`  ( Base `  K
) )  /\  ( R `  F )  =/=  ( R `  G
) ) )  -> 
( ( R `  F )  .\/  ( R `  ( F  o.  G ) ) )  =  ( ( R `
 F )  .\/  ( R `  G ) ) )
9312, 42, 71, 92pm2.61da3ne 2768 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( R `  F )  .\/  ( R `  ( F  o.  G )
) )  =  ( ( R `  F
)  .\/  ( R `  G ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2644   class class class wbr 4393    _I cid 4732    |` cres 4943    o. ccom 4945   -->wf 5515   -1-1-onto->wf1o 5518   ` cfv 5519  (class class class)co 6193   Basecbs 14285   lecple 14356   joincjn 15225   0.cp0 15318   Latclat 15326   OLcol 33128   Atomscatm 33217   HLchlt 33304   LHypclh 33937   LTrncltrn 34054   trLctrl 34111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-riotaBAD 32913
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-iin 4275  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-riota 6154  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-1st 6680  df-2nd 6681  df-undef 6895  df-map 7319  df-poset 15227  df-plt 15239  df-lub 15255  df-glb 15256  df-join 15257  df-meet 15258  df-p0 15320  df-p1 15321  df-lat 15327  df-clat 15389  df-oposet 33130  df-ol 33132  df-oml 33133  df-covers 33220  df-ats 33221  df-atl 33252  df-cvlat 33276  df-hlat 33305  df-llines 33451  df-lplanes 33452  df-lvols 33453  df-lines 33454  df-psubsp 33456  df-pmap 33457  df-padd 33749  df-lhyp 33941  df-laut 33942  df-ldil 34057  df-ltrn 34058  df-trl 34112
This theorem is referenced by:  trljco2  34694  cdlemkid1  34875
  Copyright terms: Public domain W3C validator