Metamath Proof Explorer

Theorem cdleme0nex

Description: Part of proof of Lemma E in Crawley p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p \/ q/0 (i.e. the sublattice from 0 to p \/ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a - which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012)

Ref Expression
Hypotheses cdleme0nex.l 
|- .<_ = ( le ` K )
cdleme0nex.j 
|- .\/ = ( join ` K )
cdleme0nex.a 
|- A = ( Atoms ` K )
Assertion cdleme0nex 
|- ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R = P \/ R = Q ) )

Proof

Step Hyp Ref Expression
1 cdleme0nex.l 
 |-  .<_ = ( le ` K )
2 cdleme0nex.j 
 |-  .\/ = ( join ` K )
3 cdleme0nex.a 
 |-  A = ( Atoms ` K )
4 simp3r 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> -. R .<_ W )
5 simp12 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> R .<_ ( P .\/ Q ) )
6 4 5 jca 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) )
7 simp3l 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> R e. A )
8 simp13 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
9 ralnex 
 |-  ( A. r e. A -. ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
10 8 9 sylibr 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> A. r e. A -. ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
11 breq1 
 |-  ( r = R -> ( r .<_ W <-> R .<_ W ) )
12 11 notbid 
 |-  ( r = R -> ( -. r .<_ W <-> -. R .<_ W ) )
13 oveq2 
 |-  ( r = R -> ( P .\/ r ) = ( P .\/ R ) )
14 oveq2 
 |-  ( r = R -> ( Q .\/ r ) = ( Q .\/ R ) )
15 13 14 eqeq12d 
 |-  ( r = R -> ( ( P .\/ r ) = ( Q .\/ r ) <-> ( P .\/ R ) = ( Q .\/ R ) ) )
16 12 15 anbi12d 
 |-  ( r = R -> ( ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> ( -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) ) )
17 16 notbid 
 |-  ( r = R -> ( -. ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> -. ( -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) ) )
18 17 rspcva 
 |-  ( ( R e. A /\ A. r e. A -. ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) -> -. ( -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) )
19 7 10 18 syl2anc 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> -. ( -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) )
20 simp11 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> K e. HL )
21 hlcvl 
 |-  ( K e. HL -> K e. CvLat )
22 20 21 syl 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> K e. CvLat )
23 simp21 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> P e. A )
24 simp22 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> Q e. A )
25 simp23 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> P =/= Q )
26 3 1 2 cvlsupr2 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= Q ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
27 22 23 24 7 25 26 syl131anc 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
28 27 anbi2d 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) <-> ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )
29 19 28 mtbid 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> -. ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
30 ianor 
 |-  ( -. ( ( R =/= P /\ R =/= Q ) /\ ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) <-> ( -. ( R =/= P /\ R =/= Q ) \/ -. ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
31 df-3an 
 |-  ( ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) <-> ( ( R =/= P /\ R =/= Q ) /\ R .<_ ( P .\/ Q ) ) )
32 31 anbi2i 
 |-  ( ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) <-> ( -. R .<_ W /\ ( ( R =/= P /\ R =/= Q ) /\ R .<_ ( P .\/ Q ) ) ) )
33 an12 
 |-  ( ( -. R .<_ W /\ ( ( R =/= P /\ R =/= Q ) /\ R .<_ ( P .\/ Q ) ) ) <-> ( ( R =/= P /\ R =/= Q ) /\ ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
34 32 33 bitri 
 |-  ( ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) <-> ( ( R =/= P /\ R =/= Q ) /\ ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
35 34 notbii 
 |-  ( -. ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) <-> -. ( ( R =/= P /\ R =/= Q ) /\ ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
36 pm4.62 
 |-  ( ( ( R =/= P /\ R =/= Q ) -> -. ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) <-> ( -. ( R =/= P /\ R =/= Q ) \/ -. ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
37 30 35 36 3bitr4ri 
 |-  ( ( ( R =/= P /\ R =/= Q ) -> -. ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) <-> -. ( -. R .<_ W /\ ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
38 29 37 sylibr 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( R =/= P /\ R =/= Q ) -> -. ( -. R .<_ W /\ R .<_ ( P .\/ Q ) ) ) )
39 6 38 mt2d 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> -. ( R =/= P /\ R =/= Q ) )
40 neanior 
 |-  ( ( R =/= P /\ R =/= Q ) <-> -. ( R = P \/ R = Q ) )
41 40 con2bii 
 |-  ( ( R = P \/ R = Q ) <-> -. ( R =/= P /\ R =/= Q ) )
42 39 41 sylibr 
 |-  ( ( ( K e. HL /\ R .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R = P \/ R = Q ) )