Metamath Proof Explorer

Theorem cdlemf1

Description: Part of Lemma F in Crawley p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013)

Ref Expression
Hypotheses cdlemf1.l 
|- .<_ = ( le ` K )
cdlemf1.j 
|- .\/ = ( join ` K )
cdlemf1.a 
|- A = ( Atoms ` K )
cdlemf1.h 
|- H = ( LHyp ` K )
Assertion cdlemf1 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ U .<_ ( P .\/ q ) ) )

Proof

Step Hyp Ref Expression
1 cdlemf1.l 
 |-  .<_ = ( le ` K )
2 cdlemf1.j 
 |-  .\/ = ( join ` K )
3 cdlemf1.a 
 |-  A = ( Atoms ` K )
4 cdlemf1.h 
 |-  H = ( LHyp ` K )
5 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL )
6 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A )
7 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> U e. A )
8 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> U .<_ W )
9 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> -. P .<_ W )
10 nbrne2 
 |-  ( ( U .<_ W /\ -. P .<_ W ) -> U =/= P )
11 10 necomd 
 |-  ( ( U .<_ W /\ -. P .<_ W ) -> P =/= U )
12 8 9 11 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> P =/= U )
13 1 2 3 hlsupr 
 |-  ( ( ( K e. HL /\ P e. A /\ U e. A ) /\ P =/= U ) -> E. q e. A ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) )
14 5 6 7 12 13 syl31anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) )
15 simp31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> q =/= P )
16 15 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> P =/= q )
17 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> -. P .<_ W )
18 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> U .<_ W )
19 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> K e. HL )
20 19 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> K e. Lat )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 21 3 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
23 22 3ad2ant2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> q e. ( Base ` K ) )
24 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> U e. A )
25 21 3 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> U e. ( Base ` K ) )
27 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> W e. H )
28 21 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
29 27 28 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> W e. ( Base ` K ) )
30 21 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( q e. ( Base ` K ) /\ U e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( q .<_ W /\ U .<_ W ) <-> ( q .\/ U ) .<_ W ) )
31 20 23 26 29 30 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( ( q .<_ W /\ U .<_ W ) <-> ( q .\/ U ) .<_ W ) )
32 31 biimpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( ( q .<_ W /\ U .<_ W ) -> ( q .\/ U ) .<_ W ) )
33 18 32 mpan2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( q .<_ W -> ( q .\/ U ) .<_ W ) )
34 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> q .<_ ( P .\/ U ) )
35 hlcvl 
 |-  ( K e. HL -> K e. CvLat )
36 19 35 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> K e. CvLat )
37 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> q e. A )
38 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> P e. A )
39 simp32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> q =/= U )
40 1 2 3 cvlatexch2 
 |-  ( ( K e. CvLat /\ ( q e. A /\ P e. A /\ U e. A ) /\ q =/= U ) -> ( q .<_ ( P .\/ U ) -> P .<_ ( q .\/ U ) ) )
41 36 37 38 24 39 40 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( q .<_ ( P .\/ U ) -> P .<_ ( q .\/ U ) ) )
42 34 41 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> P .<_ ( q .\/ U ) )
43 21 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
44 38 43 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> P e. ( Base ` K ) )
45 21 2 3 hlatjcl 
 |-  ( ( K e. HL /\ q e. A /\ U e. A ) -> ( q .\/ U ) e. ( Base ` K ) )
46 19 37 24 45 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( q .\/ U ) e. ( Base ` K ) )
47 21 1 lattr 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( q .\/ U ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .<_ ( q .\/ U ) /\ ( q .\/ U ) .<_ W ) -> P .<_ W ) )
48 20 44 46 29 47 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( ( P .<_ ( q .\/ U ) /\ ( q .\/ U ) .<_ W ) -> P .<_ W ) )
49 42 48 mpand 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( ( q .\/ U ) .<_ W -> P .<_ W ) )
50 33 49 syld 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( q .<_ W -> P .<_ W ) )
51 17 50 mtod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> -. q .<_ W )
52 1 2 3 cvlatexch1 
 |-  ( ( K e. CvLat /\ ( q e. A /\ U e. A /\ P e. A ) /\ q =/= P ) -> ( q .<_ ( P .\/ U ) -> U .<_ ( P .\/ q ) ) )
53 36 37 24 38 15 52 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( q .<_ ( P .\/ U ) -> U .<_ ( P .\/ q ) ) )
54 34 53 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> U .<_ ( P .\/ q ) )
55 16 51 54 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ q e. A /\ ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) ) -> ( P =/= q /\ -. q .<_ W /\ U .<_ ( P .\/ q ) ) )
56 55 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( q e. A -> ( ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) -> ( P =/= q /\ -. q .<_ W /\ U .<_ ( P .\/ q ) ) ) ) )
57 56 reximdvai 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( E. q e. A ( q =/= P /\ q =/= U /\ q .<_ ( P .\/ U ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ U .<_ ( P .\/ q ) ) ) )
58 14 57 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ U .<_ ( P .\/ q ) ) )