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

Theorem cdleme20c 33791
Description: Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line.  D,  F,  Y,  G represent s2, f(s), t2, f(t). (Contributed by NM, 15-Nov-2012.)
Hypotheses
Ref Expression
cdleme19.l  |-  .<_  =  ( le `  K )
cdleme19.j  |-  .\/  =  ( join `  K )
cdleme19.m  |-  ./\  =  ( meet `  K )
cdleme19.a  |-  A  =  ( Atoms `  K )
cdleme19.h  |-  H  =  ( LHyp `  K
)
cdleme19.u  |-  U  =  ( ( P  .\/  Q )  ./\  W )
cdleme19.f  |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
) )
cdleme19.g  |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
) )
cdleme19.d  |-  D  =  ( ( R  .\/  S )  ./\  W )
cdleme19.y  |-  Y  =  ( ( R  .\/  T )  ./\  W )
cdleme20.v  |-  V  =  ( ( S  .\/  T )  ./\  W )
Assertion
Ref Expression
cdleme20c  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( D  .\/  Y )  =  ( ( ( R 
.\/  S )  .\/  T )  ./\  W )
)

Proof of Theorem cdleme20c
StepHypRef Expression
1 simp1l 1029 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  K  e.  HL )
2 simp21l 1122 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  R  e.  A )
3 simp22l 1124 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  S  e.  A )
4 eqid 2420 . . . . . . . . . 10  |-  ( Base `  K )  =  (
Base `  K )
5 cdleme19.j . . . . . . . . . 10  |-  .\/  =  ( join `  K )
6 cdleme19.a . . . . . . . . . 10  |-  A  =  ( Atoms `  K )
74, 5, 6hlatjcl 32845 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  R  e.  A  /\  S  e.  A )  ->  ( R  .\/  S
)  e.  ( Base `  K ) )
81, 2, 3, 7syl3anc 1264 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( R  .\/  S )  e.  ( Base `  K
) )
9 simp1r 1030 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  W  e.  H )
10 cdleme19.h . . . . . . . . . 10  |-  H  =  ( LHyp `  K
)
114, 10lhpbase 33476 . . . . . . . . 9  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
129, 11syl 17 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  W  e.  ( Base `  K
) )
13 cdleme19.l . . . . . . . . . 10  |-  .<_  =  ( le `  K )
1413, 5, 6hlatlej1 32853 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  R  e.  A  /\  S  e.  A )  ->  R  .<_  ( R  .\/  S ) )
151, 2, 3, 14syl3anc 1264 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  R  .<_  ( R  .\/  S
) )
16 cdleme19.m . . . . . . . . 9  |-  ./\  =  ( meet `  K )
174, 13, 5, 16, 6atmod2i1 33339 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( R  e.  A  /\  ( R  .\/  S
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  R  .<_  ( R  .\/  S
) )  ->  (
( ( R  .\/  S )  ./\  W )  .\/  R )  =  ( ( R  .\/  S
)  ./\  ( W  .\/  R ) ) )
181, 2, 8, 12, 15, 17syl131anc 1277 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( ( R  .\/  S )  ./\  W )  .\/  R )  =  ( ( R  .\/  S
)  ./\  ( W  .\/  R ) ) )
19 simp21 1038 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( R  e.  A  /\  -.  R  .<_  W ) )
20 eqid 2420 . . . . . . . . . 10  |-  ( 1.
`  K )  =  ( 1. `  K
)
2113, 5, 20, 6, 10lhpjat1 33498 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R  e.  A  /\  -.  R  .<_  W ) )  -> 
( W  .\/  R
)  =  ( 1.
`  K ) )
221, 9, 19, 21syl21anc 1263 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( W  .\/  R )  =  ( 1. `  K
) )
2322oveq2d 6313 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  ./\  ( W  .\/  R ) )  =  ( ( R  .\/  S )  ./\  ( 1. `  K ) ) )
24 hlol 32840 . . . . . . . . 9  |-  ( K  e.  HL  ->  K  e.  OL )
251, 24syl 17 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  K  e.  OL )
264, 16, 20olm11 32706 . . . . . . . 8  |-  ( ( K  e.  OL  /\  ( R  .\/  S )  e.  ( Base `  K
) )  ->  (
( R  .\/  S
)  ./\  ( 1. `  K ) )  =  ( R  .\/  S
) )
2725, 8, 26syl2anc 665 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  ./\  ( 1. `  K ) )  =  ( R  .\/  S
) )
2818, 23, 273eqtrrd 2466 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( R  .\/  S )  =  ( ( ( R 
.\/  S )  ./\  W )  .\/  R ) )
2928oveq1d 6312 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  .\/  T )  =  ( ( ( ( R  .\/  S
)  ./\  W )  .\/  R )  .\/  T
) )
30 simp22r 1125 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  -.  S  .<_  W )
31 simp3r 1034 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  R  .<_  ( P  .\/  Q
) )
32 simp3l 1033 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  -.  S  .<_  ( P  .\/  Q ) )
33 eqid 2420 . . . . . . . 8  |-  ( ( R  .\/  S ) 
./\  W )  =  ( ( R  .\/  S )  ./\  W )
3413, 5, 16, 6, 10, 33cdlemeda 33777 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( R  e.  A  /\  R  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q
) ) )  -> 
( ( R  .\/  S )  ./\  W )  e.  A )
351, 9, 3, 30, 2, 31, 32, 34syl223anc 1290 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  ./\  W )  e.  A )
36 simp23 1040 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  T  e.  A )
375, 6hlatjass 32848 . . . . . 6  |-  ( ( K  e.  HL  /\  ( ( ( R 
.\/  S )  ./\  W )  e.  A  /\  R  e.  A  /\  T  e.  A )
)  ->  ( (
( ( R  .\/  S )  ./\  W )  .\/  R )  .\/  T
)  =  ( ( ( R  .\/  S
)  ./\  W )  .\/  ( R  .\/  T
) ) )
381, 35, 2, 36, 37syl13anc 1266 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( ( ( R 
.\/  S )  ./\  W )  .\/  R ) 
.\/  T )  =  ( ( ( R 
.\/  S )  ./\  W )  .\/  ( R 
.\/  T ) ) )
3929, 38eqtrd 2461 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  .\/  T )  =  ( ( ( R  .\/  S ) 
./\  W )  .\/  ( R  .\/  T ) ) )
4039oveq1d 6312 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( ( R  .\/  S )  .\/  T ) 
./\  W )  =  ( ( ( ( R  .\/  S ) 
./\  W )  .\/  ( R  .\/  T ) )  ./\  W )
)
414, 5, 6hlatjcl 32845 . . . . 5  |-  ( ( K  e.  HL  /\  R  e.  A  /\  T  e.  A )  ->  ( R  .\/  T
)  e.  ( Base `  K ) )
421, 2, 36, 41syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( R  .\/  T )  e.  ( Base `  K
) )
43 hllat 32842 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
441, 43syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  K  e.  Lat )
454, 13, 16latmle2 16301 . . . . 5  |-  ( ( K  e.  Lat  /\  ( R  .\/  S )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( R  .\/  S )  ./\  W )  .<_  W )
4644, 8, 12, 45syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( R  .\/  S
)  ./\  W )  .<_  W )
474, 13, 5, 16, 6atmod1i1 33335 . . . 4  |-  ( ( K  e.  HL  /\  ( ( ( R 
.\/  S )  ./\  W )  e.  A  /\  ( R  .\/  T )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  /\  ( ( R  .\/  S )  ./\  W )  .<_  W )  ->  ( ( ( R 
.\/  S )  ./\  W )  .\/  ( ( R  .\/  T ) 
./\  W ) )  =  ( ( ( ( R  .\/  S
)  ./\  W )  .\/  ( R  .\/  T
) )  ./\  W
) )
481, 35, 42, 12, 46, 47syl131anc 1277 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( ( R  .\/  S )  ./\  W )  .\/  ( ( R  .\/  T )  ./\  W )
)  =  ( ( ( ( R  .\/  S )  ./\  W )  .\/  ( R  .\/  T
) )  ./\  W
) )
4940, 48eqtr4d 2464 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  (
( ( R  .\/  S )  .\/  T ) 
./\  W )  =  ( ( ( R 
.\/  S )  ./\  W )  .\/  ( ( R  .\/  T ) 
./\  W ) ) )
50 cdleme19.d . . 3  |-  D  =  ( ( R  .\/  S )  ./\  W )
51 cdleme19.y . . 3  |-  Y  =  ( ( R  .\/  T )  ./\  W )
5250, 51oveq12i 6309 . 2  |-  ( D 
.\/  Y )  =  ( ( ( R 
.\/  S )  ./\  W )  .\/  ( ( R  .\/  T ) 
./\  W ) )
5349, 52syl6reqr 2480 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A
)  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) )  ->  ( D  .\/  Y )  =  ( ( ( R 
.\/  S )  .\/  T )  ./\  W )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867   class class class wbr 4417   ` cfv 5593  (class class class)co 6297   Basecbs 15099   lecple 15175   joincjn 16167   meetcmee 16168   1.cp1 16262   Latclat 16269   OLcol 32653   Atomscatm 32742   HLchlt 32829   LHypclh 33462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-1st 6799  df-2nd 6800  df-preset 16151  df-poset 16169  df-plt 16182  df-lub 16198  df-glb 16199  df-join 16200  df-meet 16201  df-p0 16263  df-p1 16264  df-lat 16270  df-clat 16332  df-oposet 32655  df-ol 32657  df-oml 32658  df-covers 32745  df-ats 32746  df-atl 32777  df-cvlat 32801  df-hlat 32830  df-psubsp 32981  df-pmap 32982  df-padd 33274  df-lhyp 33466
This theorem is referenced by:  cdleme20d  33792
  Copyright terms: Public domain W3C validator