Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalawlem12 Structured version   Unicode version

Theorem dalawlem12 33366
 Description: Lemma for dalaw 33370. Second part of dalawlem13 33367. (Contributed by NM, 17-Sep-2012.)
Hypotheses
Ref Expression
dalawlem.l
dalawlem.j
dalawlem.m
dalawlem.a
Assertion
Ref Expression
dalawlem12

Proof of Theorem dalawlem12
StepHypRef Expression
1 eqid 2422 . . . 4
2 dalawlem.l . . . 4
3 simp11 1035 . . . . 5
4 hllat 32848 . . . . 5
53, 4syl 17 . . . 4
6 simp21 1038 . . . . . 6
7 simp22 1039 . . . . . 6
8 dalawlem.j . . . . . . 7
9 dalawlem.a . . . . . . 7
101, 8, 9hlatjcl 32851 . . . . . 6
113, 6, 7, 10syl3anc 1264 . . . . 5
12 simp31 1041 . . . . . 6
13 simp32 1042 . . . . . 6
141, 8, 9hlatjcl 32851 . . . . . 6
153, 12, 13, 14syl3anc 1264 . . . . 5
16 dalawlem.m . . . . . 6
171, 16latmcl 16286 . . . . 5
185, 11, 15, 17syl3anc 1264 . . . 4
191, 9atbase 32774 . . . . . . . 8
2012, 19syl 17 . . . . . . 7
211, 8latjcl 16285 . . . . . . 7
225, 11, 20, 21syl3anc 1264 . . . . . 6
231, 9atbase 32774 . . . . . . 7
2413, 23syl 17 . . . . . 6
251, 16latmcl 16286 . . . . . 6
265, 22, 24, 25syl3anc 1264 . . . . 5
271, 8latjcl 16285 . . . . 5
285, 26, 20, 27syl3anc 1264 . . . 4
291, 9atbase 32774 . . . . . . 7
307, 29syl 17 . . . . . 6
31 simp33 1043 . . . . . . 7
321, 8, 9hlatjcl 32851 . . . . . . 7
333, 13, 31, 32syl3anc 1264 . . . . . 6
341, 16latmcl 16286 . . . . . 6
355, 30, 33, 34syl3anc 1264 . . . . 5
361, 8, 9hlatjcl 32851 . . . . . 6
373, 31, 12, 36syl3anc 1264 . . . . 5
381, 8latjcl 16285 . . . . 5
395, 35, 37, 38syl3anc 1264 . . . 4
401, 2, 8latlej1 16294 . . . . . . 7
415, 11, 20, 40syl3anc 1264 . . . . . 6
421, 8, 9hlatjcl 32851 . . . . . . . 8
433, 13, 12, 42syl3anc 1264 . . . . . . 7
441, 2, 16latmlem1 16315 . . . . . . 7
455, 11, 22, 43, 44syl13anc 1266 . . . . . 6
4641, 45mpd 15 . . . . 5
478, 9hlatjcom 32852 . . . . . . 7
483, 12, 13, 47syl3anc 1264 . . . . . 6
4948oveq2d 6318 . . . . 5
501, 2, 8latlej2 16295 . . . . . . 7
515, 11, 20, 50syl3anc 1264 . . . . . 6
521, 2, 8, 16, 9atmod2i2 33346 . . . . . 6
533, 13, 22, 20, 51, 52syl131anc 1277 . . . . 5
5446, 49, 533brtr4d 4451 . . . 4
55 hlol 32846 . . . . . . . . . . 11
563, 55syl 17 . . . . . . . . . 10
571, 8, 9hlatjcl 32851 . . . . . . . . . . . 12
583, 6, 12, 57syl3anc 1264 . . . . . . . . . . 11
591, 8latjcl 16285 . . . . . . . . . . 11
605, 30, 58, 59syl3anc 1264 . . . . . . . . . 10
611, 8, 9hlatjcl 32851 . . . . . . . . . . 11
623, 7, 13, 61syl3anc 1264 . . . . . . . . . 10
631, 16latmassOLD 32714 . . . . . . . . . 10
6456, 60, 62, 24, 63syl13anc 1266 . . . . . . . . 9
658, 9hlatjass 32854 . . . . . . . . . . . 12
663, 6, 7, 12, 65syl13anc 1266 . . . . . . . . . . 11
678, 9hlatj12 32855 . . . . . . . . . . . 12
683, 6, 7, 12, 67syl13anc 1266 . . . . . . . . . . 11
6966, 68eqtr2d 2464 . . . . . . . . . 10
702, 8, 9hlatlej2 32860 . . . . . . . . . . . 12
713, 7, 13, 70syl3anc 1264 . . . . . . . . . . 11
721, 2, 16latleeqm2 16314 . . . . . . . . . . . 12
735, 24, 62, 72syl3anc 1264 . . . . . . . . . . 11
7471, 73mpbid 213 . . . . . . . . . 10
7569, 74oveq12d 6320 . . . . . . . . 9
7664, 75eqtr2d 2464 . . . . . . . 8
772, 8, 9hlatlej1 32859 . . . . . . . . . . . 12
783, 7, 13, 77syl3anc 1264 . . . . . . . . . . 11
791, 2, 8, 16, 9atmod1i1 33341 . . . . . . . . . . 11
803, 7, 58, 62, 78, 79syl131anc 1277 . . . . . . . . . 10
812, 8, 9hlatlej2 32860 . . . . . . . . . . . 12
823, 31, 7, 81syl3anc 1264 . . . . . . . . . . 11
83 simp13 1037 . . . . . . . . . . . 12
84 simp12 1036 . . . . . . . . . . . . . 14
8584oveq1d 6317 . . . . . . . . . . . . 13
868, 9hlatjcom 32852 . . . . . . . . . . . . . 14
873, 7, 31, 86syl3anc 1264 . . . . . . . . . . . . 13
8885, 87eqtr3d 2465 . . . . . . . . . . . 12
8983, 88breqtrd 4445 . . . . . . . . . . 11
901, 16latmcl 16286 . . . . . . . . . . . . 13
915, 58, 62, 90syl3anc 1264 . . . . . . . . . . . 12
921, 8, 9hlatjcl 32851 . . . . . . . . . . . . 13
933, 31, 7, 92syl3anc 1264 . . . . . . . . . . . 12
941, 2, 8latjle12 16296 . . . . . . . . . . . 12
955, 30, 91, 93, 94syl13anc 1266 . . . . . . . . . . 11
9682, 89, 95mpbi2and 929 . . . . . . . . . 10
9780, 96eqbrtrrd 4443 . . . . . . . . 9
982, 8, 9hlatlej1 32859 . . . . . . . . . 10
993, 13, 31, 98syl3anc 1264 . . . . . . . . 9
1001, 16latmcl 16286 . . . . . . . . . . 11
1015, 60, 62, 100syl3anc 1264 . . . . . . . . . 10
1021, 2, 16latmlem12 16317 . . . . . . . . . 10
1035, 101, 93, 24, 33, 102syl122anc 1273 . . . . . . . . 9
10497, 99, 103mp2and 683 . . . . . . . 8
10576, 104eqbrtrd 4441 . . . . . . 7
1062, 8, 9hlatlej2 32860 . . . . . . . . . 10
1073, 13, 31, 106syl3anc 1264 . . . . . . . . 9
1081, 2, 8, 16, 9atmod1i1 33341 . . . . . . . . 9
1093, 31, 30, 33, 107, 108syl131anc 1277 . . . . . . . 8
1101, 9atbase 32774 . . . . . . . . . 10
11131, 110syl 17 . . . . . . . . 9
1121, 8latjcom 16293 . . . . . . . . 9
1135, 111, 35, 112syl3anc 1264 . . . . . . . 8
114109, 113eqtr3d 2465 . . . . . . 7
115105, 114breqtrd 4445 . . . . . 6
1161, 8latjcl 16285 . . . . . . . 8
1175, 35, 111, 116syl3anc 1264 . . . . . . 7
1181, 2, 8latjlej1 16299 . . . . . . 7
1195, 26, 117, 20, 118syl13anc 1266 . . . . . 6
120115, 119mpd 15 . . . . 5
1211, 8latjass 16329 . . . . . 6
1225, 35, 111, 20, 121syl13anc 1266 . . . . 5
123120, 122breqtrd 4445 . . . 4
1241, 2, 5, 18, 28, 39, 54, 123lattrd 16292 . . 3
1251, 2, 16latmle1 16310 . . . 4
1265, 11, 15, 125syl3anc 1264 . . 3
1271, 2, 16latlem12 16312 . . . 4
1285, 18, 39, 11, 127syl13anc 1266 . . 3
129124, 126, 128mpbi2and 929 . 2
1301, 9atbase 32774 . . . . . 6
1316, 130syl 17 . . . . 5
1321, 2, 8, 16latmlej12 16325 . . . . 5
1335, 30, 33, 131, 132syl13anc 1266 . . . 4
1341, 2, 8, 16, 9llnmod1i2 33344 . . . 4
1353, 35, 11, 31, 12, 133, 134syl321anc 1286 . . 3
1368, 9hlatjidm 32853 . . . . . . 7
1373, 7, 136syl2anc 665 . . . . . 6
13884oveq2d 6318 . . . . . 6
139137, 138eqtr3d 2465 . . . . 5
140139oveq1d 6317 . . . 4
1411, 16latmcom 16309 . . . . . 6
1425, 37, 11, 141syl3anc 1264 . . . . 5
1438, 9hlatjcom 32852 . . . . . . . 8
1443, 6, 7, 143syl3anc 1264 . . . . . . 7
14584oveq1d 6317 . . . . . . 7
146144, 145eqtrd 2463 . . . . . 6
147146oveq1d 6317 . . . . 5
148142, 147eqtrd 2463 . . . 4
149140, 148oveq12d 6320 . . 3
150135, 149eqtr3d 2465 . 2
151129, 150breqtrd 4445 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1868   class class class wbr 4420  cfv 5598  (class class class)co 6302  cbs 15109  cple 15185  cjn 16177  cmee 16178  clat 16279  col 32659  catm 32748  chlt 32835 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-preset 16161  df-poset 16179  df-plt 16192  df-lub 16208  df-glb 16209  df-join 16210  df-meet 16211  df-p0 16273  df-lat 16280  df-clat 16342  df-oposet 32661  df-ol 32663  df-oml 32664  df-covers 32751  df-ats 32752  df-atl 32783  df-cvlat 32807  df-hlat 32836  df-psubsp 32987  df-pmap 32988  df-padd 33280 This theorem is referenced by:  dalawlem13  33367
 Copyright terms: Public domain W3C validator