Metamath Proof Explorer


Theorem cdlemk49

Description: Part of proof of Lemma K of Crawley p. 118. Line 5, p. 120. G , I stand for g, h. X represents tau. (Contributed by NM, 23-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 cdlemk49 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXI/gXP˙G/gXP˙RI/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 simp11 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBKHLWH
13 simp12 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBFTFIB
14 simp13 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBGTGIB
15 simp21 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBNT
16 simp22 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBPA¬P˙W
17 simp23 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRF=RN
18 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNG/gXT
19 12 13 14 15 16 17 18 syl132anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXT
20 simp3 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBITIIB
21 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s KHLWHFTFIBITIIBNTPA¬P˙WRF=RNI/gXT
22 12 13 20 15 16 17 21 syl132anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBI/gXT
23 6 7 ltrncom KHLWHG/gXTI/gXTG/gXI/gX=I/gXG/gX
24 12 19 22 23 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXI/gX=I/gXG/gX
25 24 fveq1d KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXI/gXP=I/gXG/gXP
26 simp2 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBNTPA¬P˙WRF=RN
27 1 2 3 4 5 6 7 8 9 10 11 cdlemk48 KHLWHFTFIBITIIBNTPA¬P˙WRF=RNGTGIBI/gXG/gXP˙G/gXP˙RI/gX
28 12 13 20 26 14 27 syl311anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBI/gXG/gXP˙G/gXP˙RI/gX
29 25 28 eqbrtrd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXI/gXP˙G/gXP˙RI/gX