Metamath Proof Explorer


Theorem cdleme21d

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 115, 3rd line. D , F , N , E , B , Z represent s_2, f(s), f_s(r), z_2, f(z), f_z(r) respectively. We prove f_s(r) = f_z(r). (Contributed by NM, 29-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ˙=K
cdleme21.j ˙=joinK
cdleme21.m ˙=meetK
cdleme21.a A=AtomsK
cdleme21.h H=LHypK
cdleme21.u U=P˙Q˙W
cdleme21.f F=S˙U˙Q˙P˙S˙W
cdleme21.b B=z˙U˙Q˙P˙z˙W
cdleme21.d D=R˙S˙W
cdleme21.e E=R˙z˙W
cdleme21d.n N=P˙Q˙F˙D
cdleme21d.z Z=P˙Q˙B˙E
Assertion cdleme21d KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zN=Z

Proof

Step Hyp Ref Expression
1 cdleme21.l ˙=K
2 cdleme21.j ˙=joinK
3 cdleme21.m ˙=meetK
4 cdleme21.a A=AtomsK
5 cdleme21.h H=LHypK
6 cdleme21.u U=P˙Q˙W
7 cdleme21.f F=S˙U˙Q˙P˙S˙W
8 cdleme21.b B=z˙U˙Q˙P˙z˙W
9 cdleme21.d D=R˙S˙W
10 cdleme21.e E=R˙z˙W
11 cdleme21d.n N=P˙Q˙F˙D
12 cdleme21d.z Z=P˙Q˙B˙E
13 simp11 KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zKHLWH
14 simp12 KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zPA¬P˙W
15 simp13 KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zQA¬Q˙W
16 simp2l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zRA¬R˙W
17 simp2r KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zSA¬S˙W
18 simp33l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zzA¬z˙W
19 simp31 KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zPQ
20 simp11l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zKHL
21 simp12l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zPA
22 simp13l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zQA
23 simp2rl KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zSA
24 simp32l KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙z¬S˙P˙Q
25 18 simpld KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zzA
26 simp33r KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zP˙z=S˙z
27 1 2 4 cdleme21a KHLPAQASA¬S˙P˙QzAP˙z=S˙zSz
28 20 21 22 23 24 25 26 27 syl322anc KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zSz
29 19 28 jca KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zPQSz
30 1 2 4 cdleme21b KHLPAQASAPQ¬S˙P˙QzAP˙z=S˙z¬z˙P˙Q
31 20 21 22 23 19 24 25 26 30 syl332anc KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙z¬z˙P˙Q
32 simp32r KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zR˙P˙Q
33 24 31 32 3jca KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙z¬S˙P˙Q¬z˙P˙QR˙P˙Q
34 1 2 3 4 5 6 cdleme21c KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬U˙S˙z
35 13 14 22 23 19 24 25 26 34 syl332anc KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙z¬U˙S˙z
36 eqid S˙z˙W=S˙z˙W
37 1 2 3 4 5 6 7 8 9 10 36 11 12 cdleme20 KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WzA¬z˙WPQSz¬S˙P˙Q¬z˙P˙QR˙P˙Q¬U˙S˙zN=Z
38 13 14 15 16 17 18 29 33 35 37 syl333anc KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WSA¬S˙WPQ¬S˙P˙QR˙P˙QzA¬z˙WP˙z=S˙zN=Z