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

Theorem mapdh9a 31249
 Description: Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 31250? (Contributed by NM, 14-May-2015.)
Hypotheses
Ref Expression
mapdh8a.h
mapdh8a.u
mapdh8a.v
mapdh8a.s
mapdh8a.o
mapdh8a.n
mapdh8a.c LCDual
mapdh8a.d
mapdh8a.r
mapdh8a.q
mapdh8a.j
mapdh8a.m mapd
mapdh8a.i
mapdh8a.k
mapdh8h.f
mapdh8h.mn
mapdh9a.x
mapdh9a.t
Assertion
Ref Expression
mapdh9a
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,,   ,,   ,,   ,   ,,   ,   ,,   ,   ,,   ,   ,   ,,   ,,   ,,   ,,   , ,   ,,   ,   ,,   ,,   ,,   ,,
Dummy variable is distinct from all other variables.
Allowed substitution groups:   ()   (,,)   (,,)   (,)   (,)   (,,,)   (,)   (,,,)   (,)   (,)   ()   (,,,)

Proof of Theorem mapdh9a
StepHypRef Expression
1 mapdh8a.h . . . . . . 7
2 mapdh8a.u . . . . . . 7
3 mapdh8a.v . . . . . . 7
4 mapdh8a.s . . . . . . 7
5 mapdh8a.o . . . . . . 7
6 mapdh8a.n . . . . . . 7
7 mapdh8a.c . . . . . . 7 LCDual
8 mapdh8a.d . . . . . . 7
9 mapdh8a.r . . . . . . 7
10 mapdh8a.q . . . . . . 7
11 mapdh8a.j . . . . . . 7
12 mapdh8a.m . . . . . . 7 mapd
13 mapdh8a.i . . . . . . 7
14 mapdh8a.k . . . . . . . 8
15143ad2ant1 978 . . . . . . 7
16 mapdh8h.f . . . . . . . 8
17163ad2ant1 978 . . . . . . 7
18 mapdh8h.mn . . . . . . . 8
19183ad2ant1 978 . . . . . . 7
20 mapdh9a.x . . . . . . . 8
21203ad2ant1 978 . . . . . . 7
22 simp3ll 1028 . . . . . . 7
23 simp3rl 1030 . . . . . . 7
24 simplrl 738 . . . . . . . . 9
25243ad2ant3 980 . . . . . . . 8
2625necomd 2532 . . . . . . 7
27 simprrl 742 . . . . . . . . 9
28273ad2ant3 980 . . . . . . . 8
2928necomd 2532 . . . . . . 7
30 simplrr 739 . . . . . . . 8
31303ad2ant3 980 . . . . . . 7
32 simprrr 743 . . . . . . . 8
33323ad2ant3 980 . . . . . . 7
34 mapdh9a.t . . . . . . . 8
35343ad2ant1 978 . . . . . . 7
361, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 17, 19, 21, 22, 23, 26, 29, 31, 33, 35mapdh8 31248 . . . . . 6
37363exp 1152 . . . . 5
3837ralrimivv 2637 . . . 4
39 eldifi 3301 . . . . . . . . 9
4020, 39syl 17 . . . . . . . 8
411, 2, 3, 6, 14, 40, 34dvh3dim 30905 . . . . . . 7
42 eqid 2286 . . . . . . . . . . 11
431, 2, 14dvhlmod 30569 . . . . . . . . . . . 12
4443ad2antrr 708 . . . . . . . . . . 11
453, 42, 6, 43, 40, 34lspprcl 15731 . . . . . . . . . . . 12
4645ad2antrr 708 . . . . . . . . . . 11
47 simplr 733 . . . . . . . . . . 11
48 simpr 449 . . . . . . . . . . 11
493, 5, 42, 44, 46, 47, 48lssneln0 15705 . . . . . . . . . 10
501, 2, 14dvhlvec 30568 . . . . . . . . . . . 12
5150ad2antrr 708 . . . . . . . . . . 11
5240ad2antrr 708 . . . . . . . . . . 11
5334ad2antrr 708 . . . . . . . . . . 11
543, 6, 51, 47, 52, 53, 48lspindpi 15881 . . . . . . . . . 10
5549, 54jca 520 . . . . . . . . 9
5655ex 425 . . . . . . . 8
5756reximdva 2658 . . . . . . 7
5841, 57mpd 16 . . . . . 6
5914ad2antrr 708 . . . . . . . . . 10
6016ad2antrr 708 . . . . . . . . . . 11
6118ad2antrr 708 . . . . . . . . . . 11
6220ad2antrr 708 . . . . . . . . . . 11
63 simplr 733 . . . . . . . . . . 11
64 simprrl 742 . . . . . . . . . . . 12
6564necomd 2532 . . . . . . . . . . 11
6610, 13, 1, 12, 2, 3, 4, 5, 6, 7, 8, 9, 11, 59, 60, 61, 62, 63, 65mapdhcl 31186 . . . . . . . . . 10
67 eqidd 2287 . . . . . . . . . . . 12
68 simprl 734 . . . . . . . . . . . . 13
6910, 13, 1, 12, 2, 3, 4, 5, 6, 7, 8, 9, 11, 59, 60, 61, 62, 68, 66, 65mapdheq 31187 . . . . . . . . . . . 12
7067, 69mpbid 203 . . . . . . . . . . 11
7170simpld 447 . . . . . . . . . 10
7234ad2antrr 708 . . . . . . . . . 10
73 simprrr 743 . . . . . . . . . 10
7410, 13, 1, 12, 2, 3, 4, 5, 6, 7, 8, 9, 11, 59, 66, 71, 68, 72, 73mapdhcl 31186 . . . . . . . . 9
7574ex 425 . . . . . . . 8
7675ancld 538 . . . . . . 7
7776reximdva 2658 . . . . . 6
7858, 77mpd 16 . . . . 5
79 eleq1 2346 . . . . . . 7
80 sneq 3654 . . . . . . . . . 10
8180fveq2d 5491 . . . . . . . . 9
8281neeq1d 2462 . . . . . . . 8
8381neeq1d 2462 . . . . . . . 8
8482, 83anbi12d 693 . . . . . . 7
8579, 84anbi12d 693 . . . . . 6
86 oteq1 3808 . . . . . . . 8
87 oteq3 3810 . . . . . . . . . 10
8887fveq2d 5491 . . . . . . . . 9
89 oteq2 3809 . . . . . . . . 9
9088, 89syl 17 . . . . . . . 8
9186, 90eqtrd 2318 . . . . . . 7
9291fveq2d 5491 . . . . . 6
9385, 92reusv3 4543 . . . . 5
9478, 93syl 17 . . . 4
9538, 94mpbid 203 . . 3
96 ioran 478 . . . . . . . 8
97 elun 3319 . . . . . . . 8
9896, 97xchnxbir 302 . . . . . . 7
9943ad2antrr 708 . . . . . . . . . 10
1003, 42, 6lspsncl 15730 . . . . . . . . . . . 12
10143, 40, 100syl2anc 644 . . . . . . . . . . 11
102101ad2antrr 708 . . . . . . . . . 10
103 simplr 733 . . . . . . . . . 10
104 simprl 734 . . . . . . . . . 10
1053, 5, 42, 99, 102, 103, 104lssneln0 15705 . . . . . . . . 9
106105ex 425 . . . . . . . 8
10743ad2antrr 708 . . . . . . . . . . 11
108 simplr 733 . . . . . . . . . . 11
10940ad2antrr 708 . . . . . . . . . . 11
110 simpr 449 . . . . . . . . . . 11
1113, 6, 107, 108, 109, 110lspsnne2 15867 . . . . . . . . . 10
112111ex 425 . . . . . . . . 9
11343ad2antrr 708 . . . . . . . . . . 11
114 simplr 733 . . . . . . . . . . 11
11534ad2antrr 708 . . . . . . . . . . 11
116 simpr 449 . . . . . . . . . . 11
1173, 6, 113, 114, 115, 116lspsnne2 15867 . . . . . . . . . 10
118117ex 425 . . . . . . . . 9
119112, 118anim12d 548 . . . . . . . 8
120106, 119jcad 521 . . . . . . 7
12198, 120syl5bi 210 . . . . . 6
122121imim1d 71 . . . . 5
123122ralimdva 2624 . . . 4
124123reximdv 2657 . . 3
12595, 124mpd 16 . 2
1263, 6, 43, 40, 34lspprid1 15750 . . . . . . . . 9
12742, 6, 43, 45, 126lspsnel5a 15749 . . . . . . . 8
1283, 6, 43, 40, 34lspprid2 15751 . . . . . . . . 9
12942, 6, 43, 45, 128lspsnel5a 15749 . . . . . . . 8
130127, 129unssd 3354 . . . . . . 7
131130sseld 3182 . . . . . 6
132131con3d 127 . . . . 5
133132reximdv 2657 . . . 4
13441, 133mpd 16 . . 3
135 reusv1 4535 . . 3
136134, 135syl 17 . 2
137125, 136mpbird 225 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wb 178   wo 359   wa 360   w3a 936   wceq 1625   wcel 1687   wne 2449  wral 2546  wrex 2547  wreu 2548  cvv 2791   cdif 3152   cun 3153  cif 3568  csn 3643  cpr 3644  cotp 3647   cmpt 4080  cfv 5223  (class class class)co 5821  c1st 6083  c2nd 6084  crio 6292  cbs 13144  c0g 13396  csg 14361  clmod 15623  clss 15685  clspn 15724  clvec 15851  chlt 28809  clh 29442  cdvh 30537  LCDualclcd 31045  mapdcmpd 31083 This theorem is referenced by:  hdmap1eulem  31283 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-rep 4134  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-cnex 8790  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810  ax-pre-mulgt0 8811 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-fal 1313  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-reu 2553  df-rmo 2554  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-ot 3653  df-uni 3831  df-int 3866  df-iun 3910  df-iin 3911  df-br 4027  df-opab 4081  df-mpt 4082  df-tr 4117  df-eprel 4306  df-id 4310  df-po 4315  df-so 4316  df-fr 4353  df-we 4355  df-ord 4396  df-on 4397  df-lim 4398  df-suc 4399  df-om 4658  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-of 6041  df-1st 6085  df-2nd 6086  df-tpos 6197  df-iota 6254  df-undef 6293  df-riota 6301  df-recs 6385  df-rdg 6420  df-1o 6476  df-oadd 6480  df-er 6657  df-map 6771  df-en 6861  df-dom 6862  df-sdom 6863  df-fin 6864  df-pnf 8866  df-mnf 8867  df-xr 8868  df-ltxr 8869  df-le 8870  df-sub 9036  df-neg 9037  df-nn 9744  df-2 9801  df-3 9802  df-4 9803  df-5 9804  df-6 9805  df-n0 9963  df-z 10022  df-uz 10228  df-fz 10779  df-struct 13146  df-ndx 13147  df-slot 13148  df-base 13149  df-sets 13150  df-ress 13151  df-plusg 13217  df-mulr 13218  df-sca 13220  df-vsca 13221  df-0g 13400  df-mre 13484  df-mrc 13485  df-acs 13487  df-poset 14076  df-plt 14088  df-lub 14104  df-glb 14105  df-join 14106  df-meet 14107  df-p0 14141  df-p1 14142  df-lat 14148  df-clat 14210  df-mnd 14363  df-submnd 14412  df-grp 14485  df-minusg 14486  df-sbg 14487  df-subg 14614  df-cntz 14789  df-oppg 14815  df-lsm 14943  df-cmn 15087  df-abl 15088  df-mgp 15322  df-rng 15336  df-ur 15338  df-oppr 15401  df-dvdsr 15419  df-unit 15420  df-invr 15450  df-dvr 15461  df-drng 15510  df-lmod 15625  df-lss 15686  df-lsp 15725  df-lvec 15852  df-lsatoms 28435  df-lshyp 28436  df-lcv 28478  df-lfl 28517  df-lkr 28545  df-ldual 28583  df-oposet 28635  df-ol 28637  df-oml 28638  df-covers 28725  df-ats 28726  df-atl 28757  df-cvlat 28781  df-hlat 28810  df-llines 28956  df-lplanes 28957  df-lvols 28958  df-lines 28959  df-psubsp 28961  df-pmap 28962  df-padd 29254  df-lhyp 29446  df-laut 29447  df-ldil 29562  df-ltrn 29563  df-trl 29617  df-tgrp 30201  df-tendo 30213  df-edring 30215  df-dveca 30461  df-disoa 30488  df-dvech 30538  df-dib 30598  df-dic 30632  df-dih 30688  df-doch 30807  df-djh 30854  df-lcdual 31046  df-mapd 31084
 Copyright terms: Public domain W3C validator