Metamath Proof Explorer


Theorem cdleme41sn3aw

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is different on and off the P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme41.b B=BaseK
cdleme41.l ˙=K
cdleme41.j ˙=joinK
cdleme41.m ˙=meetK
cdleme41.a A=AtomsK
cdleme41.h H=LHypK
cdleme41.u U=P˙Q˙W
cdleme41.d D=s˙U˙Q˙P˙s˙W
cdleme41.e E=t˙U˙Q˙P˙t˙W
cdleme41.g G=P˙Q˙E˙s˙t˙W
cdleme41.i I=ιyB|tA¬t˙W¬t˙P˙Qy=G
cdleme41.n N=ifs˙P˙QID
Assertion cdleme41sn3aw KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSR/sNS/sN

Proof

Step Hyp Ref Expression
1 cdleme41.b B=BaseK
2 cdleme41.l ˙=K
3 cdleme41.j ˙=joinK
4 cdleme41.m ˙=meetK
5 cdleme41.a A=AtomsK
6 cdleme41.h H=LHypK
7 cdleme41.u U=P˙Q˙W
8 cdleme41.d D=s˙U˙Q˙P˙s˙W
9 cdleme41.e E=t˙U˙Q˙P˙t˙W
10 cdleme41.g G=P˙Q˙E˙s˙t˙W
11 cdleme41.i I=ιyB|tA¬t˙W¬t˙P˙Qy=G
12 cdleme41.n N=ifs˙P˙QID
13 simp1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSKHLWHPA¬P˙WQA¬Q˙W
14 simp21 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSPQ
15 simp22 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSRA¬R˙W
16 simp31 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSR˙P˙Q
17 eqid P˙Q˙E˙R˙t˙W=P˙Q˙E˙R˙t˙W
18 eqid ιyB|tA¬t˙W¬t˙P˙Qy=P˙Q˙E˙R˙t˙W=ιyB|tA¬t˙W¬t˙P˙Qy=P˙Q˙E˙R˙t˙W
19 1 2 3 4 5 6 7 8 9 10 11 12 17 18 cdleme41sn3a KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/sN˙P˙Q
20 13 14 15 16 19 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSR/sN˙P˙Q
21 simp23 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSSA¬S˙W
22 simp32 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRS¬S˙P˙Q
23 1 2 3 4 5 6 7 8 12 cdleme35sn3a KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙Q¬S/sN˙P˙Q
24 13 14 21 22 23 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRS¬S/sN˙P˙Q
25 nbrne2 R/sN˙P˙Q¬S/sN˙P˙QR/sNS/sN
26 20 24 25 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRSR/sNS/sN