Metamath Proof Explorer


Theorem cdleme19c

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, 1st line. D , F represent s_2, f(s). We prove f(s) =/= s_2. (Contributed by NM, 13-Nov-2012)

Ref Expression
Hypotheses cdleme19.l ˙=K
cdleme19.j ˙=joinK
cdleme19.m ˙=meetK
cdleme19.a A=AtomsK
cdleme19.h H=LHypK
cdleme19.u U=P˙Q˙W
cdleme19.f F=S˙U˙Q˙P˙S˙W
cdleme19.g G=T˙U˙Q˙P˙T˙W
cdleme19.d D=R˙S˙W
cdleme19.y Y=R˙T˙W
Assertion cdleme19c KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QFD

Proof

Step Hyp Ref Expression
1 cdleme19.l ˙=K
2 cdleme19.j ˙=joinK
3 cdleme19.m ˙=meetK
4 cdleme19.a A=AtomsK
5 cdleme19.h H=LHypK
6 cdleme19.u U=P˙Q˙W
7 cdleme19.f F=S˙U˙Q˙P˙S˙W
8 cdleme19.g G=T˙U˙Q˙P˙T˙W
9 cdleme19.d D=R˙S˙W
10 cdleme19.y Y=R˙T˙W
11 simp1l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QKHL
12 11 hllatd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QKLat
13 simp31 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QRA
14 simp23l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QSA
15 eqid BaseK=BaseK
16 15 2 4 hlatjcl KHLRASAR˙SBaseK
17 11 13 14 16 syl3anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QR˙SBaseK
18 simp1r KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QWH
19 15 5 lhpbase WHWBaseK
20 18 19 syl KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QWBaseK
21 15 1 3 latmle2 KLatR˙SBaseKWBaseKR˙S˙W˙W
22 12 17 20 21 syl3anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QR˙S˙W˙W
23 9 22 eqbrtrid KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QD˙W
24 simp32 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QPQ
25 simp33 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙Q¬S˙P˙Q
26 24 25 jca KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QPQ¬S˙P˙Q
27 1 2 3 4 5 6 7 cdleme3 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙Q¬F˙W
28 26 27 syld3an3 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙Q¬F˙W
29 nbrne2 D˙W¬F˙WDF
30 23 28 29 syl2anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QDF
31 30 necomd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WRAPQ¬S˙P˙QFD