Metamath Proof Explorer

Theorem cdlemg7fvbwN

Description: Properties of a translation of an element not under W . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw ? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg4.l 
|- .<_ = ( le ` K )
cdlemg4.a 
|- A = ( Atoms ` K )
cdlemg4.h 
|- H = ( LHyp ` K )
cdlemg4.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemg4.b 
|- B = ( Base ` K )
Assertion cdlemg7fvbwN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) -> ( ( F ` X ) e. B /\ -. ( F ` X ) .<_ W ) )

Proof

Step Hyp Ref Expression
1 cdlemg4.l 
 |-  .<_ = ( le ` K )
2 cdlemg4.a 
 |-  A = ( Atoms ` K )
3 cdlemg4.h 
 |-  H = ( LHyp ` K )
4 cdlemg4.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 cdlemg4.b 
 |-  B = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( meet ` K ) = ( meet ` K )
8 5 1 6 7 2 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. r e. A ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) )
9 8 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) -> E. r e. A ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) )
10 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( K e. HL /\ W e. H ) )
11 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> r e. A )
12 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> -. r .<_ W )
13 11 12 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( r e. A /\ -. r .<_ W ) )
14 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( X e. B /\ -. X .<_ W ) )
15 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> F e. T )
16 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X )
17 3 4 1 6 2 7 5 cdlemg2fv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( F e. T /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` X ) = ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) )
18 10 13 14 15 16 17 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` X ) = ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) )
19 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> K e. HL )
20 19 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> K e. Lat )
21 1 2 3 4 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( r e. A /\ -. r .<_ W ) ) -> ( ( F ` r ) e. A /\ -. ( F ` r ) .<_ W ) )
22 21 simpld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( r e. A /\ -. r .<_ W ) ) -> ( F ` r ) e. A )
23 10 15 13 22 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` r ) e. A )
24 5 2 atbase 
 |-  ( ( F ` r ) e. A -> ( F ` r ) e. B )
25 23 24 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` r ) e. B )
26 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> X e. B )
27 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> W e. H )
28 5 3 lhpbase 
 |-  ( W e. H -> W e. B )
29 27 28 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> W e. B )
30 5 7 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ( meet ` K ) W ) e. B )
31 20 26 29 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( X ( meet ` K ) W ) e. B )
32 5 6 latjcl 
 |-  ( ( K e. Lat /\ ( F ` r ) e. B /\ ( X ( meet ` K ) W ) e. B ) -> ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) e. B )
33 20 25 31 32 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) e. B )
34 18 33 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` X ) e. B )
35 21 simprd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( r e. A /\ -. r .<_ W ) ) -> -. ( F ` r ) .<_ W )
36 10 15 13 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> -. ( F ` r ) .<_ W )
37 5 1 6 latlej1 
 |-  ( ( K e. Lat /\ ( F ` r ) e. B /\ ( X ( meet ` K ) W ) e. B ) -> ( F ` r ) .<_ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) )
38 20 25 31 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( F ` r ) .<_ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) )
39 5 1 lattr 
 |-  ( ( K e. Lat /\ ( ( F ` r ) e. B /\ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) e. B /\ W e. B ) ) -> ( ( ( F ` r ) .<_ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) /\ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) .<_ W ) -> ( F ` r ) .<_ W ) )
40 20 25 33 29 39 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( ( ( F ` r ) .<_ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) /\ ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) .<_ W ) -> ( F ` r ) .<_ W ) )
41 38 40 mpand 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) .<_ W -> ( F ` r ) .<_ W ) )
42 36 41 mtod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> -. ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) .<_ W )
43 18 breq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( ( F ` X ) .<_ W <-> ( ( F ` r ) ( join ` K ) ( X ( meet ` K ) W ) ) .<_ W ) )
44 42 43 mtbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> -. ( F ` X ) .<_ W )
45 34 44 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) /\ r e. A /\ ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( ( F ` X ) e. B /\ -. ( F ` X ) .<_ W ) )
46 45 rexlimdv3a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) -> ( E. r e. A ( -. r .<_ W /\ ( r ( join ` K ) ( X ( meet ` K ) W ) ) = X ) -> ( ( F ` X ) e. B /\ -. ( F ` X ) .<_ W ) ) )
47 9 46 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ F e. T ) -> ( ( F ` X ) e. B /\ -. ( F ` X ) .<_ W ) )