Metamath Proof Explorer


Theorem cdlemki

Description: Part of proof of Lemma K of Crawley p. 118. TODO: Eliminate and put into cdlemksel . (Contributed by NM, 25-Jun-2013)

Ref Expression
Hypotheses cdlemk.b B=BaseK
cdlemk.l ˙=K
cdlemk.j ˙=joinK
cdlemk.a A=AtomsK
cdlemk.h H=LHypK
cdlemk.t T=LTrnKW
cdlemk.r R=trLKW
cdlemk.m ˙=meetK
cdlemk.i I=ιiT|iP=P˙RG˙NP˙RGF-1
Assertion cdlemki KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFIT

Proof

Step Hyp Ref Expression
1 cdlemk.b B=BaseK
2 cdlemk.l ˙=K
3 cdlemk.j ˙=joinK
4 cdlemk.a A=AtomsK
5 cdlemk.h H=LHypK
6 cdlemk.t T=LTrnKW
7 cdlemk.r R=trLKW
8 cdlemk.m ˙=meetK
9 cdlemk.i I=ιiT|iP=P˙RG˙NP˙RGF-1
10 simp11 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFKHLWH
11 simp22 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFPA¬P˙W
12 simp1 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFKHLWHFTGT
13 simp21 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFNT
14 2 4 5 6 ltrnel KHLWHNTPA¬P˙WNPA¬NP˙W
15 10 13 11 14 syl3anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFNPA¬NP˙W
16 simp11l KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFKHL
17 simp22l KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFPA
18 14 simpld KHLWHNTPA¬P˙WNPA
19 10 13 11 18 syl3anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFNPA
20 2 3 4 hlatlej2 KHLPANPANP˙P˙NP
21 16 17 19 20 syl3anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFNP˙P˙NP
22 simp23 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFRF=RN
23 22 oveq2d KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFP˙RF=P˙RN
24 2 3 4 5 6 7 trljat1 KHLWHNTPA¬P˙WP˙RN=P˙NP
25 10 13 11 24 syl3anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFP˙RN=P˙NP
26 23 25 eqtr2d KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFP˙NP=P˙RF
27 21 26 breqtrd KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFNP˙P˙RF
28 simp31 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFFIB
29 simp32 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFGIB
30 simp33 KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFRGRF
31 30 necomd KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFRFRG
32 eqid P˙RG˙NP˙RGF-1=P˙RG˙NP˙RGF-1
33 1 2 3 8 4 5 6 7 32 cdlemh KHLWHFTGTPA¬P˙WNPA¬NP˙WNP˙P˙RFFIBGIBRFRGP˙RG˙NP˙RGF-1A¬P˙RG˙NP˙RGF-1˙W
34 12 11 15 27 28 29 31 33 syl133anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFP˙RG˙NP˙RGF-1A¬P˙RG˙NP˙RGF-1˙W
35 2 4 5 6 9 ltrniotacl KHLWHPA¬P˙WP˙RG˙NP˙RGF-1A¬P˙RG˙NP˙RGF-1˙WIT
36 10 11 34 35 syl3anc KHLWHFTGTNTPA¬P˙WRF=RNFIBGIBRGRFIT