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 ˙ = K
cdleme0nex.j ˙ = join K
cdleme0nex.a A = Atoms K
Assertion cdleme0nex K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W R = P R = Q

Proof

Step Hyp Ref Expression
1 cdleme0nex.l ˙ = K
2 cdleme0nex.j ˙ = join K
3 cdleme0nex.a A = Atoms K
4 simp3r K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W ¬ R ˙ W
5 simp12 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W R ˙ P ˙ Q
6 4 5 jca K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W ¬ R ˙ W R ˙ P ˙ Q
7 simp3l K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W R A
8 simp13 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r
9 ralnex r A ¬ ¬ r ˙ W P ˙ r = Q ˙ r ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r
10 8 9 sylibr K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W r 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 A r A ¬ ¬ r ˙ W P ˙ r = Q ˙ r ¬ ¬ R ˙ W P ˙ R = Q ˙ R
19 7 10 18 syl2anc K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W ¬ ¬ R ˙ W P ˙ R = Q ˙ R
20 simp11 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W K HL
21 hlcvl K HL K CvLat
22 20 21 syl K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W K CvLat
23 simp21 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W P A
24 simp22 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W Q A
25 simp23 K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W P Q
26 3 1 2 cvlsupr2 K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R P R Q R ˙ P ˙ Q
27 22 23 24 7 25 26 syl131anc K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W P ˙ R = Q ˙ R R P R Q R ˙ P ˙ Q
28 27 anbi2d K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W ¬ R ˙ W P ˙ R = Q ˙ R ¬ R ˙ W R P R Q R ˙ P ˙ Q
29 19 28 mtbid K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R 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 HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W R P R Q ¬ ¬ R ˙ W R ˙ P ˙ Q
39 6 38 mt2d K HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R 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 HL R ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q R A ¬ R ˙ W R = P R = Q