Metamath Proof Explorer


Theorem cdlemk55

Description: Part of proof of Lemma K of Crawley p. 118. Line 11, p. 120. G , I stand for g, h. X represents tau. (Contributed by NM, 26-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b B=BaseK
cdlemk5.l ˙=K
cdlemk5.j ˙=joinK
cdlemk5.m ˙=meetK
cdlemk5.a A=AtomsK
cdlemk5.h H=LHypK
cdlemk5.t T=LTrnKW
cdlemk5.r R=trLKW
cdlemk5.z Z=P˙Rb˙NP˙RbF-1
cdlemk5.y Y=P˙Rg˙Z˙Rgb-1
cdlemk5.x X=ιzT|bTbIBRbRFRbRgzP=Y
Assertion cdlemk55 KHLWHRF=RNFTFIBNTGTITPA¬P˙WGI/gX=G/gXI/gX

Proof

Step Hyp Ref Expression
1 cdlemk5.b B=BaseK
2 cdlemk5.l ˙=K
3 cdlemk5.j ˙=joinK
4 cdlemk5.m ˙=meetK
5 cdlemk5.a A=AtomsK
6 cdlemk5.h H=LHypK
7 cdlemk5.t T=LTrnKW
8 cdlemk5.r R=trLKW
9 cdlemk5.z Z=P˙Rb˙NP˙RbF-1
10 cdlemk5.y Y=P˙Rg˙Z˙Rgb-1
11 cdlemk5.x X=ιzT|bTbIBRbRFRbRgzP=Y
12 simpl1 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIKHLWHRF=RN
13 simpl21 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIFTFIBNT
14 simpl22 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIGT
15 simpl3 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIPA¬P˙W
16 simpl23 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIIT
17 simpr KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIRG=RI
18 1 2 3 4 5 6 7 8 9 10 11 cdlemk55b KHLWHRF=RNFTFIBNTGTPA¬P˙WITRG=RIGI/gX=G/gXI/gX
19 12 13 14 15 16 17 18 syl132anc KHLWHRF=RNFTFIBNTGTITPA¬P˙WRG=RIGI/gX=G/gXI/gX
20 simpl1 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIKHLWHRF=RN
21 simpl21 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIFTFIBNT
22 simpl22 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIGT
23 simpl3 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIPA¬P˙W
24 simpl23 KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIIT
25 simpr KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIRGRI
26 1 2 3 4 5 6 7 8 9 10 11 cdlemk53 KHLWHRF=RNFTFIBNTGTPA¬P˙WITRGRIGI/gX=G/gXI/gX
27 20 21 22 23 24 25 26 syl132anc KHLWHRF=RNFTFIBNTGTITPA¬P˙WRGRIGI/gX=G/gXI/gX
28 19 27 pm2.61dane KHLWHRF=RNFTFIBNTGTITPA¬P˙WGI/gX=G/gXI/gX