![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > mapdpglem21 | Structured version Visualization version Unicode version |
Description: Lemma for mapdpg 35345. (Contributed by NM, 20-Mar-2015.) |
Ref | Expression |
---|---|
mapdpglem.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.m |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.c |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.y |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem1.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem2.j |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.te |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.t |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem3.e |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.q |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem.ne |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.jt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.z |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.g4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.z4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.t4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem4.xn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem12.yn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mapdpglem17.ep |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mapdpglem21 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapdpglem4.t4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | oveq2d 6324 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mapdpglem3.f |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | mapdpglem3.t |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2471 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eqid 2471 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | mapdpglem3.r |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | mapdpglem.h |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | mapdpglem.c |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | mapdpglem.k |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 8, 9, 10 | lcdlmod 35231 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | mapdpglem.u |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 8, 12, 10 | dvhlvec 34748 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | mapdpglem3.a |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 14 | lvecdrng 18406 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 13, 15 | syl 17 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | mapdpglem4.g4 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | mapdpglem.m |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | mapdpglem.v |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | mapdpglem.s |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
21 | mapdpglem.n |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
22 | mapdpglem.x |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | mapdpglem.y |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
24 | mapdpglem1.p |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
25 | mapdpglem2.j |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
26 | mapdpglem3.te |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
27 | mapdpglem3.b |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
28 | mapdpglem3.g |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
29 | mapdpglem3.e |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
30 | mapdpglem4.q |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
31 | mapdpglem.ne |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
32 | mapdpglem4.jt |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
33 | mapdpglem4.z |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
34 | mapdpglem4.z4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
35 | mapdpglem4.xn |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
36 | 8, 18, 12, 19, 20, 21, 9, 10, 22, 23, 24, 25, 3, 26, 14, 27, 4, 7, 28, 29, 30, 31, 32, 33, 17, 34, 1, 35 | mapdpglem11 35321 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | eqid 2471 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
38 | 27, 33, 37 | drnginvrcl 18070 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 16, 17, 36, 38 | syl3anc 1292 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 8, 12, 14, 27, 9, 5, 6, 10 | lcdsbase 35239 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 39, 40 | eleqtrrd 2552 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 8, 12, 14, 27, 9, 3, 4, 10, 17, 28 | lcdvscl 35244 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | eqid 2471 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
44 | eqid 2471 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
45 | 8, 12, 10 | dvhlmod 34749 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | 19, 43, 21 | lspsncl 18278 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
47 | 45, 23, 46 | syl2anc 673 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
48 | 8, 18, 12, 43, 9, 44, 10, 47 | mapdcl2 35295 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | 3, 44 | lssss 18238 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | 48, 49 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
51 | 50, 34 | sseldd 3419 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 3, 4, 5, 6, 7, 11, 41, 42, 51 | lmodsubdi 18223 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
53 | eqid 2471 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
54 | eqid 2471 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
55 | 27, 33, 53, 54, 37 | drnginvrr 18073 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
56 | 16, 17, 36, 55 | syl3anc 1292 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
57 | eqid 2471 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
58 | 8, 12, 14, 54, 9, 5, 57, 10 | lcd1 35248 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
59 | 56, 58 | eqtr4d 2508 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
60 | 59 | oveq1d 6323 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
61 | 8, 12, 14, 27, 53, 9, 3, 4, 10, 39, 17, 28 | lcdvsass 35246 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
62 | 3, 5, 4, 57 | lmodvs1 18197 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
63 | 11, 28, 62 | syl2anc 673 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
64 | 60, 61, 63 | 3eqtr3d 2513 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
65 | 64 | oveq1d 6323 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
66 | mapdpglem17.ep |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
67 | 66 | oveq2i 6319 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
68 | 65, 67 | syl6eqr 2523 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
69 | 2, 52, 68 | 3eqtrd 2509 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-riotaBAD 32589 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-tpos 6991 df-undef 7038 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-sca 15284 df-vsca 15285 df-0g 15418 df-mre 15570 df-mrc 15571 df-acs 15573 df-preset 16251 df-poset 16269 df-plt 16282 df-lub 16298 df-glb 16299 df-join 16300 df-meet 16301 df-p0 16363 df-p1 16364 df-lat 16370 df-clat 16432 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-grp 16751 df-minusg 16752 df-sbg 16753 df-subg 16892 df-cntz 17049 df-oppg 17075 df-lsm 17366 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-ring 17860 df-oppr 17929 df-dvdsr 17947 df-unit 17948 df-invr 17978 df-dvr 17989 df-drng 18055 df-lmod 18171 df-lss 18234 df-lsp 18273 df-lvec 18404 df-lsatoms 32613 df-lshyp 32614 df-lcv 32656 df-lfl 32695 df-lkr 32723 df-ldual 32761 df-oposet 32813 df-ol 32815 df-oml 32816 df-covers 32903 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988 df-llines 33134 df-lplanes 33135 df-lvols 33136 df-lines 33137 df-psubsp 33139 df-pmap 33140 df-padd 33432 df-lhyp 33624 df-laut 33625 df-ldil 33740 df-ltrn 33741 df-trl 33796 df-tgrp 34381 df-tendo 34393 df-edring 34395 df-dveca 34641 df-disoa 34668 df-dvech 34718 df-dib 34778 df-dic 34812 df-dih 34868 df-doch 34987 df-djh 35034 df-lcdual 35226 df-mapd 35264 |
This theorem is referenced by: mapdpglem22 35332 |
Copyright terms: Public domain | W3C validator |