Metamath Proof Explorer

Theorem cdlemn2

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

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

Proof

Step Hyp Ref Expression
1 cdlemn2.b 
 |-  B = ( Base ` K )
2 cdlemn2.l 
 |-  .<_ = ( le ` K )
3 cdlemn2.j 
 |-  .\/ = ( join ` K )
4 cdlemn2.a 
 |-  A = ( Atoms ` K )
5 cdlemn2.h 
 |-  H = ( LHyp ` K )
6 cdlemn2.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemn2.r 
 |-  R = ( ( trL ` K ) ` W )
8 cdlemn2.f 
 |-  F = ( iota_ h e. T ( h ` Q ) = S )
9 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( K e. HL /\ W e. H ) )
10 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( Q e. A /\ -. Q .<_ W ) )
11 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( S e. A /\ -. S .<_ W ) )
12 2 4 5 6 8 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> F e. T )
13 9 10 11 12 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> F e. T )
14 eqid 
 |-  ( meet ` K ) = ( meet ` K )
15 2 3 14 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( R ` F ) = ( ( Q .\/ ( F ` Q ) ) ( meet ` K ) W ) )
16 9 13 10 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( R ` F ) = ( ( Q .\/ ( F ` Q ) ) ( meet ` K ) W ) )
17 2 4 5 6 8 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( F ` Q ) = S )
18 9 10 11 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( F ` Q ) = S )
19 18 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( Q .\/ ( F ` Q ) ) = ( Q .\/ S ) )
20 19 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( ( Q .\/ ( F ` Q ) ) ( meet ` K ) W ) = ( ( Q .\/ S ) ( meet ` K ) W ) )
21 16 20 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( R ` F ) = ( ( Q .\/ S ) ( meet ` K ) W ) )
22 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> K e. HL )
23 22 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> K e. Lat )
24 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> Q e. A )
25 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> Q e. B )
27 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> X e. B )
28 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> Q .<_ ( Q .\/ X ) )
29 23 26 27 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> Q .<_ ( Q .\/ X ) )
30 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> S .<_ ( Q .\/ X ) )
31 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> S e. A )
32 1 4 atbase 
 |-  ( S e. A -> S e. B )
33 31 32 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> S e. B )
34 1 3 latjcl 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q .\/ X ) e. B )
35 23 26 27 34 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( Q .\/ X ) e. B )
36 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( Q e. B /\ S e. B /\ ( Q .\/ X ) e. B ) ) -> ( ( Q .<_ ( Q .\/ X ) /\ S .<_ ( Q .\/ X ) ) <-> ( Q .\/ S ) .<_ ( Q .\/ X ) ) )
37 23 26 33 35 36 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( ( Q .<_ ( Q .\/ X ) /\ S .<_ ( Q .\/ X ) ) <-> ( Q .\/ S ) .<_ ( Q .\/ X ) ) )
38 29 30 37 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( Q .\/ S ) .<_ ( Q .\/ X ) )
39 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ S e. A ) -> ( Q .\/ S ) e. B )
40 22 24 31 39 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( Q .\/ S ) e. B )
41 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> W e. H )
42 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
43 41 42 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> W e. B )
44 1 2 14 latmlem1 
 |-  ( ( K e. Lat /\ ( ( Q .\/ S ) e. B /\ ( Q .\/ X ) e. B /\ W e. B ) ) -> ( ( Q .\/ S ) .<_ ( Q .\/ X ) -> ( ( Q .\/ S ) ( meet ` K ) W ) .<_ ( ( Q .\/ X ) ( meet ` K ) W ) ) )
45 23 40 35 43 44 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( ( Q .\/ S ) .<_ ( Q .\/ X ) -> ( ( Q .\/ S ) ( meet ` K ) W ) .<_ ( ( Q .\/ X ) ( meet ` K ) W ) ) )
46 38 45 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( ( Q .\/ S ) ( meet ` K ) W ) .<_ ( ( Q .\/ X ) ( meet ` K ) W ) )
47 21 46 eqbrtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( R ` F ) .<_ ( ( Q .\/ X ) ( meet ` K ) W ) )
48 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( X e. B /\ X .<_ W ) )
49 1 2 3 14 4 5 lhple 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( Q .\/ X ) ( meet ` K ) W ) = X )
50 9 10 48 49 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( ( Q .\/ X ) ( meet ` K ) W ) = X )
51 47 50 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( R ` F ) .<_ X )