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

Theorem cdlemg10c 34118
Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.)
Hypotheses
Ref Expression
cdlemg8.l  |-  .<_  =  ( le `  K )
cdlemg8.j  |-  .\/  =  ( join `  K )
cdlemg8.m  |-  ./\  =  ( meet `  K )
cdlemg8.a  |-  A  =  ( Atoms `  K )
cdlemg8.h  |-  H  =  ( LHyp `  K
)
cdlemg8.t  |-  T  =  ( ( LTrn `  K
) `  W )
cdlemg10.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
cdlemg10c  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( ( G `  P ) 
.\/  ( G `  Q ) )  <->  ( R `  F )  .<_  ( P 
.\/  Q ) ) )

Proof of Theorem cdlemg10c
StepHypRef Expression
1 simp1 1005 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
2 simp3l 1033 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  F  e.  T )
3 cdlemg8.l . . . . 5  |-  .<_  =  ( le `  K )
4 cdlemg8.h . . . . 5  |-  H  =  ( LHyp `  K
)
5 cdlemg8.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
6 cdlemg10.r . . . . 5  |-  R  =  ( ( trL `  K
) `  W )
73, 4, 5, 6trlle 33662 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  .<_  W )
81, 2, 7syl2anc 665 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( R `  F
)  .<_  W )
98biantrud 509 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( ( G `  P ) 
.\/  ( G `  Q ) )  <->  ( ( R `  F )  .<_  ( ( G `  P )  .\/  ( G `  Q )
)  /\  ( R `  F )  .<_  W ) ) )
10 simp1l 1029 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  K  e.  HL )
11 hllat 32841 . . . 4  |-  ( K  e.  HL  ->  K  e.  Lat )
1210, 11syl 17 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  K  e.  Lat )
13 eqid 2423 . . . . 5  |-  ( Base `  K )  =  (
Base `  K )
1413, 4, 5, 6trlcl 33642 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  e.  (
Base `  K )
)
151, 2, 14syl2anc 665 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( R `  F
)  e.  ( Base `  K ) )
16 simp3r 1034 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  G  e.  T )
17 simp2ll 1072 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  P  e.  A )
18 cdlemg8.a . . . . . 6  |-  A  =  ( Atoms `  K )
193, 18, 4, 5ltrnat 33617 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  P  e.  A
)  ->  ( G `  P )  e.  A
)
201, 16, 17, 19syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( G `  P
)  e.  A )
21 simp2rl 1074 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  Q  e.  A )
223, 18, 4, 5ltrnat 33617 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  Q  e.  A
)  ->  ( G `  Q )  e.  A
)
231, 16, 21, 22syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( G `  Q
)  e.  A )
24 cdlemg8.j . . . . 5  |-  .\/  =  ( join `  K )
2513, 24, 18hlatjcl 32844 . . . 4  |-  ( ( K  e.  HL  /\  ( G `  P )  e.  A  /\  ( G `  Q )  e.  A )  ->  (
( G `  P
)  .\/  ( G `  Q ) )  e.  ( Base `  K
) )
2610, 20, 23, 25syl3anc 1264 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( G `  P )  .\/  ( G `  Q )
)  e.  ( Base `  K ) )
27 simp1r 1030 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  W  e.  H )
2813, 4lhpbase 33475 . . . 4  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
2927, 28syl 17 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  W  e.  ( Base `  K ) )
30 cdlemg8.m . . . 4  |-  ./\  =  ( meet `  K )
3113, 3, 30latlem12 16262 . . 3  |-  ( ( K  e.  Lat  /\  ( ( R `  F )  e.  (
Base `  K )  /\  ( ( G `  P )  .\/  ( G `  Q )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( ( R `
 F )  .<_  ( ( G `  P )  .\/  ( G `  Q )
)  /\  ( R `  F )  .<_  W )  <-> 
( R `  F
)  .<_  ( ( ( G `  P ) 
.\/  ( G `  Q ) )  ./\  W ) ) )
3212, 15, 26, 29, 31syl13anc 1266 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( ( R `
 F )  .<_  ( ( G `  P )  .\/  ( G `  Q )
)  /\  ( R `  F )  .<_  W )  <-> 
( R `  F
)  .<_  ( ( ( G `  P ) 
.\/  ( G `  Q ) )  ./\  W ) ) )
3313, 24, 18hlatjcl 32844 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
3410, 17, 21, 33syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( P  .\/  Q
)  e.  ( Base `  K ) )
3513, 3, 30latlem12 16262 . . . 4  |-  ( ( K  e.  Lat  /\  ( ( R `  F )  e.  (
Base `  K )  /\  ( P  .\/  Q
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( ( R `
 F )  .<_  ( P  .\/  Q )  /\  ( R `  F )  .<_  W )  <-> 
( R `  F
)  .<_  ( ( P 
.\/  Q )  ./\  W ) ) )
3612, 15, 34, 29, 35syl13anc 1266 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( ( R `
 F )  .<_  ( P  .\/  Q )  /\  ( R `  F )  .<_  W )  <-> 
( R `  F
)  .<_  ( ( P 
.\/  Q )  ./\  W ) ) )
378biantrud 509 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( P 
.\/  Q )  <->  ( ( R `  F )  .<_  ( P  .\/  Q
)  /\  ( R `  F )  .<_  W ) ) )
383, 24, 30, 18, 4, 5cdlemg10b 34114 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  G  e.  T )  ->  (
( ( G `  P )  .\/  ( G `  Q )
)  ./\  W )  =  ( ( P 
.\/  Q )  ./\  W ) )
39383adant3l 1260 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( ( G `
 P )  .\/  ( G `  Q ) )  ./\  W )  =  ( ( P 
.\/  Q )  ./\  W ) )
4039breq2d 4373 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( ( ( G `  P
)  .\/  ( G `  Q ) )  ./\  W )  <->  ( R `  F )  .<_  ( ( P  .\/  Q ) 
./\  W ) ) )
4136, 37, 403bitr4rd 289 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( ( ( G `  P
)  .\/  ( G `  Q ) )  ./\  W )  <->  ( R `  F )  .<_  ( P 
.\/  Q ) ) )
429, 32, 413bitrd 282 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( R `  F )  .<_  ( ( G `  P ) 
.\/  ( G `  Q ) )  <->  ( R `  F )  .<_  ( P 
.\/  Q ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   class class class wbr 4361   ` cfv 5539  (class class class)co 6244   Basecbs 15059   lecple 15135   joincjn 16127   meetcmee 16128   Latclat 16229   Atomscatm 32741   HLchlt 32828   LHypclh 33461   LTrncltrn 33578   trLctrl 33636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-riotaBAD 32437
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-1st 6746  df-2nd 6747  df-undef 6970  df-map 7424  df-preset 16111  df-poset 16129  df-plt 16142  df-lub 16158  df-glb 16159  df-join 16160  df-meet 16161  df-p0 16223  df-p1 16224  df-lat 16230  df-clat 16292  df-oposet 32654  df-ol 32656  df-oml 32657  df-covers 32744  df-ats 32745  df-atl 32776  df-cvlat 32800  df-hlat 32829  df-llines 32975  df-lplanes 32976  df-lvols 32977  df-lines 32978  df-psubsp 32980  df-pmap 32981  df-padd 33273  df-lhyp 33465  df-laut 33466  df-ldil 33581  df-ltrn 33582  df-trl 33637
This theorem is referenced by:  cdlemg10a  34119  cdlemg12d  34125
  Copyright terms: Public domain W3C validator