Metamath Proof Explorer


Theorem cdleme20aN

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 14-Nov-2012) (New usage is discouraged.)

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
cdleme20.v V=S˙T˙W
Assertion cdleme20aN KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QV˙D=S˙R˙T˙W

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 cdleme20.v V=S˙T˙W
12 11 oveq1i V˙D=S˙T˙W˙D
13 simp1l KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QKHL
14 simp1r KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QWH
15 simp22 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QSA
16 simp23 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙Q¬S˙W
17 simp21 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QRA
18 simp33 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QR˙P˙Q
19 simp32 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙Q¬S˙P˙Q
20 1 2 3 4 5 9 cdlemeda KHLWHSA¬S˙WRAR˙P˙Q¬S˙P˙QDA
21 13 14 15 16 17 18 19 20 syl223anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QDA
22 simp31 KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QTA
23 eqid BaseK=BaseK
24 23 2 4 hlatjcl KHLSATAS˙TBaseK
25 13 15 22 24 syl3anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙TBaseK
26 23 5 lhpbase WHWBaseK
27 14 26 syl KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QWBaseK
28 13 hllatd KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QKLat
29 23 2 4 hlatjcl KHLRASAR˙SBaseK
30 13 17 15 29 syl3anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QR˙SBaseK
31 23 1 3 latmle2 KLatR˙SBaseKWBaseKR˙S˙W˙W
32 28 30 27 31 syl3anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QR˙S˙W˙W
33 9 32 eqbrtrid KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QD˙W
34 23 1 2 3 4 atmod4i1 KHLDAS˙TBaseKWBaseKD˙WS˙T˙W˙D=S˙T˙D˙W
35 13 21 25 27 33 34 syl131anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙T˙W˙D=S˙T˙D˙W
36 1 2 3 4 5 9 cdleme10 KHLWHRASA¬S˙WS˙D=S˙R
37 13 14 17 15 16 36 syl212anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙D=S˙R
38 37 oveq1d KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙D˙T=S˙R˙T
39 2 4 hlatj32 KHLSADATAS˙D˙T=S˙T˙D
40 13 15 21 22 39 syl13anc KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙D˙T=S˙T˙D
41 38 40 eqtr3d KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙R˙T=S˙T˙D
42 41 oveq1d KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙R˙T˙W=S˙T˙D˙W
43 35 42 eqtr4d KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QS˙T˙W˙D=S˙R˙T˙W
44 12 43 eqtrid KHLWHRASA¬S˙WTA¬S˙P˙QR˙P˙QV˙D=S˙R˙T˙W