Metamath Proof Explorer


Theorem cdlemk7u

Description: Part of proof of Lemma K of Crawley p. 118. Line 5, p. 119 for the sigma_1 case. (Contributed by NM, 3-Jul-2013)

Ref Expression
Hypotheses cdlemk1.b B=BaseK
cdlemk1.l ˙=K
cdlemk1.j ˙=joinK
cdlemk1.m ˙=meetK
cdlemk1.a A=AtomsK
cdlemk1.h H=LHypK
cdlemk1.t T=LTrnKW
cdlemk1.r R=trLKW
cdlemk1.s S=fTιiT|iP=P˙Rf˙NP˙RfF-1
cdlemk1.o O=SD
cdlemk1.u U=eTιjT|jP=P˙Re˙OP˙ReD-1
cdlemk1.v V=GP˙XP˙RGD-1˙RXD-1
Assertion cdlemk7u KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUGP˙UXP˙V

Proof

Step Hyp Ref Expression
1 cdlemk1.b B=BaseK
2 cdlemk1.l ˙=K
3 cdlemk1.j ˙=joinK
4 cdlemk1.m ˙=meetK
5 cdlemk1.a A=AtomsK
6 cdlemk1.h H=LHypK
7 cdlemk1.t T=LTrnKW
8 cdlemk1.r R=trLKW
9 cdlemk1.s S=fTιiT|iP=P˙Rf˙NP˙RfF-1
10 cdlemk1.o O=SD
11 cdlemk1.u U=eTιjT|jP=P˙Re˙OP˙ReD-1
12 cdlemk1.v V=GP˙XP˙RGD-1˙RXD-1
13 simp31 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIBDIBGIB
14 simp33 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRFRGRDRXRD
15 13 14 jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIBDIBGIBRDRFRGRDRXRD
16 1 2 3 4 5 6 7 8 9 10 cdlemk6u KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBRDRFRGRDRXRDP˙GP˙OP˙RGD-1˙GP˙XP˙RGD-1˙RXD-1˙XP˙P˙RXD-1˙OP
17 15 16 syld3an3 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙GP˙OP˙RGD-1˙GP˙XP˙RGD-1˙RXD-1˙XP˙P˙RXD-1˙OP
18 simp11l KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDKHL
19 simp11r KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDWH
20 18 19 jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDKHLWH
21 simp23 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRF=RN
22 simp212 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDGT
23 simp12 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFT
24 simp13 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDDT
25 simp211 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDNT
26 23 24 25 3jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFTDTNT
27 simp331 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRF
28 simp332 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRGRD
29 28 necomd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRG
30 27 29 jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRFRDRG
31 simp311 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIB
32 simp313 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDGIB
33 simp312 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDDIB
34 31 32 33 3jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIBGIBDIB
35 simp22 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDPA¬P˙W
36 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 KHLWHRF=RNGTFTDTNTRDRFRDRGFIBGIBDIBPA¬P˙WUGP=P˙RG˙OP˙RGD-1
37 20 21 22 26 30 34 35 36 syl313anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUGP=P˙RG˙OP˙RGD-1
38 2 3 5 6 7 8 trljat1 KHLWHGTPA¬P˙WP˙RG=P˙GP
39 20 22 35 38 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙RG=P˙GP
40 39 oveq1d KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙RG˙OP˙RGD-1=P˙GP˙OP˙RGD-1
41 37 40 eqtrd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUGP=P˙GP˙OP˙RGD-1
42 18 hllatd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDKLat
43 simp213 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDXT
44 simp333 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRXRD
45 44 necomd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRX
46 27 45 jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRDRFRDRX
47 simp32 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDXIB
48 31 47 33 3jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIBXIBDIB
49 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat KHLWHRF=RNXTFTDTNTRDRFRDRXFIBXIBDIBPA¬P˙WUXPA
50 20 21 43 26 46 48 35 49 syl313anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXPA
51 1 5 atbase UXPAUXPB
52 50 51 syl KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXPB
53 simp22l KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDPA
54 1 2 3 5 6 7 8 4 12 cdlemkvcl KHLWHDTGTXTPAVB
55 18 19 24 22 43 53 54 syl231anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDVB
56 1 3 latjcom KLatUXPBVBUXP˙V=V˙UXP
57 42 52 55 56 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXP˙V=V˙UXP
58 12 a1i KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDV=GP˙XP˙RGD-1˙RXD-1
59 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 KHLWHRF=RNXTFTDTNTRDRFRDRXFIBXIBDIBPA¬P˙WUXP=P˙RX˙OP˙RXD-1
60 20 21 43 26 46 48 35 59 syl313anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXP=P˙RX˙OP˙RXD-1
61 2 3 5 6 7 8 trljat1 KHLWHXTPA¬P˙WP˙RX=P˙XP
62 20 43 35 61 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙RX=P˙XP
63 2 5 6 7 ltrnat KHLWHXTPAXPA
64 20 43 53 63 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDXPA
65 3 5 hlatjcom KHLXPAPAXP˙P=P˙XP
66 18 64 53 65 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDXP˙P=P˙XP
67 62 66 eqtr4d KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙RX=XP˙P
68 simp1 KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDKHLWHFTDT
69 25 35 21 3jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDNTPA¬P˙WRF=RN
70 31 33 27 3jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDFIBDIBRDRF
71 1 2 3 4 5 6 7 8 9 10 cdlemkoatnle KHLWHFTDTNTPA¬P˙WRF=RNFIBDIBRDRFOPA¬OP˙W
72 71 simpld KHLWHFTDTNTPA¬P˙WRF=RNFIBDIBRDRFOPA
73 68 69 70 72 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDOPA
74 43 24 jca KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDXTDT
75 5 6 7 8 trlcocnvat KHLWHXTDTRXRDRXD-1A
76 20 74 44 75 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDRXD-1A
77 3 5 hlatjcom KHLOPARXD-1AOP˙RXD-1=RXD-1˙OP
78 18 73 76 77 syl3anc KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDOP˙RXD-1=RXD-1˙OP
79 67 78 oveq12d KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDP˙RX˙OP˙RXD-1=XP˙P˙RXD-1˙OP
80 60 79 eqtrd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXP=XP˙P˙RXD-1˙OP
81 58 80 oveq12d KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDV˙UXP=GP˙XP˙RGD-1˙RXD-1˙XP˙P˙RXD-1˙OP
82 57 81 eqtrd KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUXP˙V=GP˙XP˙RGD-1˙RXD-1˙XP˙P˙RXD-1˙OP
83 17 41 82 3brtr4d KHLWHFTDTNTGTXTPA¬P˙WRF=RNFIBDIBGIBXIBRDRFRGRDRXRDUGP˙UXP˙V