Metamath Proof Explorer

Theorem cdlemn10

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 27-Feb-2014)

Ref Expression
Hypotheses cdlemn10.b 
|- B = ( Base ` K )
cdlemn10.l 
|- .<_ = ( le ` K )
cdlemn10.j 
|- .\/ = ( join ` K )
cdlemn10.a 
|- A = ( Atoms ` K )
cdlemn10.h 
|- H = ( LHyp ` K )
cdlemn10.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemn10.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemn10 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S .<_ ( Q .\/ X ) )

Proof

Step Hyp Ref Expression
1 cdlemn10.b 
 |-  B = ( Base ` K )
2 cdlemn10.l 
 |-  .<_ = ( le ` K )
3 cdlemn10.j 
 |-  .\/ = ( join ` K )
4 cdlemn10.a 
 |-  A = ( Atoms ` K )
5 cdlemn10.h 
 |-  H = ( LHyp ` K )
6 cdlemn10.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemn10.r 
 |-  R = ( ( trL ` K ) ` W )
8 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> K e. Lat )
10 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S e. A )
11 1 4 atbase 
 |-  ( S e. A -> S e. B )
12 10 11 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S e. B )
13 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> Q e. A )
14 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ S e. A ) -> ( Q .\/ S ) e. B )
15 8 13 10 14 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ S ) e. B )
16 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
17 13 16 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> Q e. B )
18 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> X e. B )
19 1 3 latjcl 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q .\/ X ) e. B )
20 9 17 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ X ) e. B )
21 2 3 4 hlatlej2 
 |-  ( ( K e. HL /\ Q e. A /\ S e. A ) -> S .<_ ( Q .\/ S ) )
22 8 13 10 21 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S .<_ ( Q .\/ S ) )
23 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> W e. H )
24 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
25 23 24 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> W e. B )
26 2 3 4 hlatlej1 
 |-  ( ( K e. HL /\ Q e. A /\ S e. A ) -> Q .<_ ( Q .\/ S ) )
27 8 13 10 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> Q .<_ ( Q .\/ S ) )
28 eqid 
 |-  ( meet ` K ) = ( meet ` K )
29 1 2 3 28 4 atmod3i1 
 |-  ( ( K e. HL /\ ( Q e. A /\ ( Q .\/ S ) e. B /\ W e. B ) /\ Q .<_ ( Q .\/ S ) ) -> ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) = ( ( Q .\/ S ) ( meet ` K ) ( Q .\/ W ) ) )
30 8 13 15 25 27 29 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) = ( ( Q .\/ S ) ( meet ` K ) ( Q .\/ W ) ) )
31 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( K e. HL /\ W e. H ) )
32 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q e. A /\ -. Q .<_ W ) )
33 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
34 2 3 33 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q .\/ W ) = ( 1. ` K ) )
35 31 32 34 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ W ) = ( 1. ` K ) )
36 35 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( Q .\/ S ) ( meet ` K ) ( Q .\/ W ) ) = ( ( Q .\/ S ) ( meet ` K ) ( 1. ` K ) ) )
37 hlol 
 |-  ( K e. HL -> K e. OL )
38 8 37 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> K e. OL )
39 1 28 33 olm11 
 |-  ( ( K e. OL /\ ( Q .\/ S ) e. B ) -> ( ( Q .\/ S ) ( meet ` K ) ( 1. ` K ) ) = ( Q .\/ S ) )
40 38 15 39 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( Q .\/ S ) ( meet ` K ) ( 1. ` K ) ) = ( Q .\/ S ) )
41 30 36 40 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ S ) = ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) )
42 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> g e. T )
43 2 3 28 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( R ` g ) = ( ( Q .\/ ( g ` Q ) ) ( meet ` K ) W ) )
44 31 42 32 43 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( R ` g ) = ( ( Q .\/ ( g ` Q ) ) ( meet ` K ) W ) )
45 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( g ` Q ) = S )
46 45 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ ( g ` Q ) ) = ( Q .\/ S ) )
47 46 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( Q .\/ ( g ` Q ) ) ( meet ` K ) W ) = ( ( Q .\/ S ) ( meet ` K ) W ) )
48 44 47 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( R ` g ) = ( ( Q .\/ S ) ( meet ` K ) W ) )
49 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( R ` g ) .<_ X )
50 48 49 eqbrtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( Q .\/ S ) ( meet ` K ) W ) .<_ X )
51 1 28 latmcl 
 |-  ( ( K e. Lat /\ ( Q .\/ S ) e. B /\ W e. B ) -> ( ( Q .\/ S ) ( meet ` K ) W ) e. B )
52 9 15 25 51 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( Q .\/ S ) ( meet ` K ) W ) e. B )
53 1 2 3 latjlej2 
 |-  ( ( K e. Lat /\ ( ( ( Q .\/ S ) ( meet ` K ) W ) e. B /\ X e. B /\ Q e. B ) ) -> ( ( ( Q .\/ S ) ( meet ` K ) W ) .<_ X -> ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) .<_ ( Q .\/ X ) ) )
54 9 52 18 17 53 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( ( ( Q .\/ S ) ( meet ` K ) W ) .<_ X -> ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) .<_ ( Q .\/ X ) ) )
55 50 54 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ ( ( Q .\/ S ) ( meet ` K ) W ) ) .<_ ( Q .\/ X ) )
56 41 55 eqbrtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> ( Q .\/ S ) .<_ ( Q .\/ X ) )
57 1 2 9 12 15 20 22 56 lattrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S .<_ ( Q .\/ X ) )