Metamath Proof Explorer


Theorem cdlemk55u1

Description: Lemma for cdlemk55u . (Contributed by NM, 31-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
cdlemk5.u U=gTifF=NgX
Assertion cdlemk55u1 KHLWHFTNTRF=RNFNGTITPA¬P˙WUGI=UGUI

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 cdlemk5.u U=gTifF=NgX
13 simp11 KHLWHFTNTRF=RNFNGTITPA¬P˙WKHLWH
14 simp21l KHLWHFTNTRF=RNFNGTITPA¬P˙WRF=RN
15 simp12 KHLWHFTNTRF=RNFNGTITPA¬P˙WFT
16 simp13 KHLWHFTNTRF=RNFNGTITPA¬P˙WNT
17 simp21r KHLWHFTNTRF=RNFNGTITPA¬P˙WFN
18 1 6 7 8 trlnid KHLWHFTNTFNRF=RNFIB
19 13 15 16 17 14 18 syl122anc KHLWHFTNTRF=RNFNGTITPA¬P˙WFIB
20 15 19 16 3jca KHLWHFTNTRF=RNFNGTITPA¬P˙WFTFIBNT
21 simp22 KHLWHFTNTRF=RNFNGTITPA¬P˙WGT
22 simp23 KHLWHFTNTRF=RNFNGTITPA¬P˙WIT
23 simp3 KHLWHFTNTRF=RNFNGTITPA¬P˙WPA¬P˙W
24 1 2 3 4 5 6 7 8 9 10 11 cdlemk55 KHLWHRF=RNFTFIBNTGTITPA¬P˙WGI/gX=G/gXI/gX
25 13 14 20 21 22 23 24 syl231anc KHLWHFTNTRF=RNFNGTITPA¬P˙WGI/gX=G/gXI/gX
26 6 7 ltrnco KHLWHGTITGIT
27 13 21 22 26 syl3anc KHLWHFTNTRF=RNFNGTITPA¬P˙WGIT
28 11 12 cdlemk40f FNGITUGI=GI/gX
29 17 27 28 syl2anc KHLWHFTNTRF=RNFNGTITPA¬P˙WUGI=GI/gX
30 11 12 cdlemk40f FNGTUG=G/gX
31 17 21 30 syl2anc KHLWHFTNTRF=RNFNGTITPA¬P˙WUG=G/gX
32 11 12 cdlemk40f FNITUI=I/gX
33 17 22 32 syl2anc KHLWHFTNTRF=RNFNGTITPA¬P˙WUI=I/gX
34 31 33 coeq12d KHLWHFTNTRF=RNFNGTITPA¬P˙WUGUI=G/gXI/gX
35 25 29 34 3eqtr4d KHLWHFTNTRF=RNFNGTITPA¬P˙WUGI=UGUI