Metamath Proof Explorer

Theorem cdleme3g

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 7-Jun-2012)

Ref Expression
Hypotheses cdleme1.l 
|- .<_ = ( le ` K )
cdleme1.j 
|- .\/ = ( join ` K )
cdleme1.m 
|- ./\ = ( meet ` K )
cdleme1.a 
|- A = ( Atoms ` K )
cdleme1.h 
|- H = ( LHyp ` K )
cdleme1.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme1.f 
|- F = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
cdleme3.3 
|- V = ( ( P .\/ R ) ./\ W )
Assertion cdleme3g 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F =/= U )

Proof

Step Hyp Ref Expression
1 cdleme1.l 
 |-  .<_ = ( le ` K )
2 cdleme1.j 
 |-  .\/ = ( join ` K )
3 cdleme1.m 
 |-  ./\ = ( meet ` K )
4 cdleme1.a 
 |-  A = ( Atoms ` K )
5 cdleme1.h 
 |-  H = ( LHyp ` K )
6 cdleme1.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme1.f 
 |-  F = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
8 cdleme3.3 
 |-  V = ( ( P .\/ R ) ./\ W )
9 1 2 3 4 5 6 7 8 cdleme3d 
 |-  F = ( ( R .\/ U ) ./\ ( Q .\/ V ) )
10 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. HL )
11 10 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. Lat )
12 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> R e. A )
13 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
14 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
15 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. A )
16 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P =/= Q )
17 1 2 3 4 5 6 lhpat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A )
18 13 14 15 16 17 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U e. A )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ U e. A ) -> ( R .\/ U ) e. ( Base ` K ) )
21 10 12 18 20 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R .\/ U ) e. ( Base ` K ) )
22 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. R .<_ ( P .\/ Q ) )
23 12 22 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ ( P .\/ Q ) ) )
24 1 2 3 4 5 6 7 8 cdleme3e 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( R e. A /\ -. R .<_ ( P .\/ Q ) ) ) ) -> V e. A )
25 13 14 15 23 24 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> V e. A )
26 19 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ V e. A ) -> ( Q .\/ V ) e. ( Base ` K ) )
27 10 15 25 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( Q .\/ V ) e. ( Base ` K ) )
28 19 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( R .\/ U ) e. ( Base ` K ) /\ ( Q .\/ V ) e. ( Base ` K ) ) -> ( ( R .\/ U ) ./\ ( Q .\/ V ) ) .<_ ( Q .\/ V ) )
29 11 21 27 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ U ) ./\ ( Q .\/ V ) ) .<_ ( Q .\/ V ) )
30 9 29 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F .<_ ( Q .\/ V ) )
31 simp22r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. Q .<_ W )
32 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ W ) )
33 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) )
34 1 2 3 4 5 6 8 cdleme0e 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U =/= V )
35 13 14 15 32 33 34 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U =/= V )
36 1 2 4 hlatexch2 
 |-  ( ( K e. HL /\ ( U e. A /\ Q e. A /\ V e. A ) /\ U =/= V ) -> ( U .<_ ( Q .\/ V ) -> Q .<_ ( U .\/ V ) ) )
37 10 18 15 25 35 36 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( U .<_ ( Q .\/ V ) -> Q .<_ ( U .\/ V ) ) )
38 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P e. A )
39 19 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
40 10 38 15 39 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
41 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> W e. H )
42 19 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
43 41 42 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
44 19 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
45 11 40 43 44 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
46 6 45 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U .<_ W )
47 19 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) e. ( Base ` K ) )
48 10 38 12 47 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P .\/ R ) e. ( Base ` K ) )
49 19 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ R ) ./\ W ) .<_ W )
50 11 48 43 49 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ R ) ./\ W ) .<_ W )
51 8 50 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> V .<_ W )
52 19 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
53 18 52 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U e. ( Base ` K ) )
54 19 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
55 25 54 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> V e. ( Base ` K ) )
56 19 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( U e. ( Base ` K ) /\ V e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( U .<_ W /\ V .<_ W ) <-> ( U .\/ V ) .<_ W ) )
57 11 53 55 43 56 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( U .<_ W /\ V .<_ W ) <-> ( U .\/ V ) .<_ W ) )
58 46 51 57 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( U .\/ V ) .<_ W )
59 19 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
60 15 59 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. ( Base ` K ) )
61 19 2 4 hlatjcl 
 |-  ( ( K e. HL /\ U e. A /\ V e. A ) -> ( U .\/ V ) e. ( Base ` K ) )
62 10 18 25 61 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( U .\/ V ) e. ( Base ` K ) )
63 19 1 lattr 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( U .\/ V ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( Q .<_ ( U .\/ V ) /\ ( U .\/ V ) .<_ W ) -> Q .<_ W ) )
64 11 60 62 43 63 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( Q .<_ ( U .\/ V ) /\ ( U .\/ V ) .<_ W ) -> Q .<_ W ) )
65 58 64 mpan2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( Q .<_ ( U .\/ V ) -> Q .<_ W ) )
66 37 65 syld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( U .<_ ( Q .\/ V ) -> Q .<_ W ) )
67 31 66 mtod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. U .<_ ( Q .\/ V ) )
68 nbrne2 
 |-  ( ( F .<_ ( Q .\/ V ) /\ -. U .<_ ( Q .\/ V ) ) -> F =/= U )
69 30 67 68 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F =/= U )