Metamath Proof Explorer


Theorem cdleme17d2

Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. F , G represent f(s), f_s(p) respectively. We show, in their notation, f_s(p)=q. TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013)

Ref Expression
Hypotheses cdlemef46.b B=BaseK
cdlemef46.l ˙=K
cdlemef46.j ˙=joinK
cdlemef46.m ˙=meetK
cdlemef46.a A=AtomsK
cdlemef46.h H=LHypK
cdlemef46.u U=P˙Q˙W
cdlemef46.d D=t˙U˙Q˙P˙t˙W
cdlemefs46.e E=P˙Q˙D˙s˙t˙W
cdlemef46.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
Assertion cdleme17d2 KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QFP=Q

Proof

Step Hyp Ref Expression
1 cdlemef46.b B=BaseK
2 cdlemef46.l ˙=K
3 cdlemef46.j ˙=joinK
4 cdlemef46.m ˙=meetK
5 cdlemef46.a A=AtomsK
6 cdlemef46.h H=LHypK
7 cdlemef46.u U=P˙Q˙W
8 cdlemef46.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs46.e E=P˙Q˙D˙s˙t˙W
10 cdlemef46.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 simp1 KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QKHLWHPA¬P˙WQA¬Q˙W
12 simp2l KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QPQ
13 simp12 KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QPA¬P˙W
14 simp2r KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QSA¬S˙W
15 simp11l KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QKHL
16 simp12l KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QPA
17 simp13l KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QQA
18 2 3 5 hlatlej1 KHLPAQAP˙P˙Q
19 15 16 17 18 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QP˙P˙Q
20 simp3 KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙Q¬S˙P˙Q
21 1 2 3 4 5 6 7 8 10 9 cdlemefs45 KHLWHPA¬P˙WQA¬Q˙WPQPA¬P˙WSA¬S˙WP˙P˙Q¬S˙P˙QFP=P/sS/tE
22 11 12 13 14 19 20 21 syl132anc KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QFP=P/sS/tE
23 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QSA
24 eqid S˙U˙Q˙P˙S˙W=S˙U˙Q˙P˙S˙W
25 eqid P˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W=P˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W
26 8 9 24 25 cdleme31sde PASAP/sS/tE=P˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W
27 16 23 26 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QP/sS/tE=P˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W
28 simp11 KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QKHLWH
29 2 3 4 5 6 7 24 25 cdleme17d1 KHLWHPA¬P˙WQASA¬S˙W¬S˙P˙QP˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W=Q
30 28 13 17 14 20 29 syl131anc KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QP˙Q˙S˙U˙Q˙P˙S˙W˙P˙S˙W=Q
31 22 27 30 3eqtrd KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QFP=Q