Metamath Proof Explorer


Theorem cdlemk42

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 20-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 cdlemk42 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGG/gXP=G/gY

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 simp13l KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGGT
13 1 2 3 4 5 6 7 8 9 10 11 cdlemk36 KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRgXP=Y
14 13 sbcth GT[˙G/g]˙KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRgXP=Y
15 sbcimg GT[˙G/g]˙KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRgXP=Y[˙G/g]˙KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRg[˙G/g]˙XP=Y
16 14 15 mpbid GT[˙G/g]˙KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRg[˙G/g]˙XP=Y
17 eleq1 g=GgTGT
18 neeq1 g=GgIBGIB
19 17 18 anbi12d g=GgTgIBGTGIB
20 19 3anbi3d g=GKHLWHFTFIBgTgIBKHLWHFTFIBGTGIB
21 fveq2 g=GRg=RG
22 21 neeq2d g=GRbRgRbRG
23 22 3anbi3d g=GbIBRbRFRbRgbIBRbRFRbRG
24 23 anbi2d g=GbTbIBRbRFRbRgbTbIBRbRFRbRG
25 20 24 3anbi13d g=GKHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRgKHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRG
26 25 sbcieg GT[˙G/g]˙KHLWHFTFIBgTgIBNTPA¬P˙WRF=RNbTbIBRbRFRbRgKHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRG
27 sbceqg GT[˙G/g]˙XP=YG/gXP=G/gY
28 csbfv12 G/gXP=G/gXG/gP
29 csbconstg GTG/gP=P
30 29 fveq2d GTG/gXG/gP=G/gXP
31 28 30 eqtrid GTG/gXP=G/gXP
32 31 eqeq1d GTG/gXP=G/gYG/gXP=G/gY
33 27 32 bitrd GT[˙G/g]˙XP=YG/gXP=G/gY
34 16 26 33 3imtr3d GTKHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGG/gXP=G/gY
35 12 34 mpcom KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGG/gXP=G/gY