Metamath Proof Explorer


Theorem cdleme41sn4aw

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is for on and off P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 19-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 cdleme41sn4aw KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙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˙W¬R˙P˙QS˙P˙QRSKHLWHPA¬P˙WQA¬Q˙W
14 simp21 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSPQ
15 simp23 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSSA¬S˙W
16 simp22 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSRA¬R˙W
17 simp32 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSS˙P˙Q
18 simp31 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRS¬R˙P˙Q
19 simp33 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSRS
20 19 necomd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSSR
21 1 2 3 4 5 6 7 8 9 10 11 12 cdleme41sn3aw KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙WRA¬R˙WS˙P˙Q¬R˙P˙QSRS/sNR/sN
22 13 14 15 16 17 18 20 21 syl133anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSS/sNR/sN
23 22 necomd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙QS˙P˙QRSR/sNS/sN