![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmap1l6d | Structured version Unicode version |
Description: Lemmma for hdmap1l6 35786. (Contributed by NM, 1-May-2015.) |
Ref | Expression |
---|---|
hdmap1l6.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6c.o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.c |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.q |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.m |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6cl.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6.mn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.xn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.yz |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.y |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.z |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.w |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
hdmap1l6d.wn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hdmap1l6d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmap1l6.h |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | hdmap1l6.c |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | hdmap1l6.k |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | lcdlmod 35556 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | hdmap1l6.u |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | hdmap1l6.v |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | hdmap1l6c.o |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | hdmap1l6.n |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | hdmap1l6.d |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | hdmap1l6.l |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | hdmap1l6.m |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | hdmap1l6.i |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | hdmap1l6.f |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | hdmap1l6.mn |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 1, 5, 3 | dvhlvec 35073 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | hdmap1l6d.w |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | 16 | eldifad 3443 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | hdmap1l6cl.x |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 18 | eldifad 3443 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | hdmap1l6d.y |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
21 | 20 | eldifad 3443 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | hdmap1l6d.wn |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | 6, 8, 15, 17, 19, 21, 22 | lspindpi 17331 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23 | simpld 459 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24 | necomd 2720 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | 1, 5, 6, 7, 8, 2, 9, 10, 11, 12, 3, 13, 14, 25, 18, 17 | hdmap1cl 35769 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | hdmap1l6.a |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
28 | hdmap1l6.q |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
29 | 9, 27, 28 | lmod0vrid 17097 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | 4, 26, 29 | syl2anc 661 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 30 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | oteq3 4173 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
33 | 32 | fveq2d 5798 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 1, 5, 6, 7, 2, 9, 28, 12, 3, 13, 19 | hdmap1val0 35764 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 33, 34 | sylan9eqr 2515 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 35 | oveq2d 6211 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | oveq2 6203 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
38 | 1, 5, 3 | dvhlmod 35074 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | hdmap1l6.p |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
40 | 6, 39, 7 | lmod0vrid 17097 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 38, 17, 40 | syl2anc 661 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 37, 41 | sylan9eqr 2515 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 42 | oteq3d 4176 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | 43 | fveq2d 5798 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 31, 36, 44 | 3eqtr4rd 2504 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | hdmap1l6.s |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
47 | hdmap1l6.r |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
48 | 3 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | 13 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | 18 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
51 | 14 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 16 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
53 | hdmap1l6d.z |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
54 | 53 | eldifad 3443 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
55 | 6, 39 | lmodvacl 17080 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
56 | 38, 21, 54, 55 | syl3anc 1219 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
57 | 56 | anim1i 568 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
58 | eldifsn 4103 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
59 | 57, 58 | sylibr 212 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
60 | hdmap1l6d.yz |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
61 | hdmap1l6d.xn |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
62 | 6, 8, 15, 19, 21, 54, 61 | lspindpi 17331 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
63 | 62 | simpld 459 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
64 | 6, 39, 7, 8, 15, 18, 20, 53, 16, 60, 63, 22 | mapdindp1 35684 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
65 | 6, 39, 7, 8, 15, 18, 20, 53, 16, 60, 63, 22 | mapdindp2 35685 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
66 | 6, 7, 8, 15, 18, 56, 17, 64, 65 | lspindp1 17332 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
67 | 66 | simprd 463 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
68 | 67 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
69 | 23 | simprd 463 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
70 | 6, 7, 8, 15, 16, 21, 69 | lspsnne1 17316 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
71 | eqid 2452 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
72 | 6, 8, 71, 38, 21, 54 | lsmpr 17288 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
73 | 60 | oveq2d 6211 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
74 | eqid 2452 |
. . . . . . . . . . . . 13
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
75 | 6, 74, 8 | lspsncl 17176 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
76 | 38, 21, 75 | syl2anc 661 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
77 | 74 | lsssubg 17156 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
78 | 38, 76, 77 | syl2anc 661 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
79 | 71 | lsmidm 16277 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
80 | 78, 79 | syl 16 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
81 | 72, 73, 80 | 3eqtr2d 2499 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
82 | 70, 81 | neleqtrrd 2565 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
83 | 6, 39, 8, 38, 21, 54, 17, 82 | lspindp4 17336 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
84 | 6, 8, 15, 17, 21, 56, 83 | lspindpi 17331 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
85 | 84 | simprd 463 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
86 | 85 | adantr 465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
87 | eqidd 2453 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
88 | eqidd 2453 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
89 | 1, 5, 6, 39, 46, 7, 8, 2, 9, 27, 47, 28, 10, 11, 12, 48, 49, 50, 51, 52, 59, 68, 86, 87, 88 | hdmap1l6a 35774 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
90 | 45, 89 | pm2.61dane 2767 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-riotaBAD 32923 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-ot 3989 df-uni 4195 df-int 4232 df-iun 4276 df-iin 4277 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-of 6425 df-om 6582 df-1st 6682 df-2nd 6683 df-tpos 6850 df-undef 6897 df-recs 6937 df-rdg 6971 df-1o 7025 df-oadd 7029 df-er 7206 df-map 7321 df-en 7416 df-dom 7417 df-sdom 7418 df-fin 7419 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-nn 10429 df-2 10486 df-3 10487 df-4 10488 df-5 10489 df-6 10490 df-n0 10686 df-z 10753 df-uz 10968 df-fz 11550 df-struct 14289 df-ndx 14290 df-slot 14291 df-base 14292 df-sets 14293 df-ress 14294 df-plusg 14365 df-mulr 14366 df-sca 14368 df-vsca 14369 df-0g 14494 df-mre 14638 df-mrc 14639 df-acs 14641 df-poset 15230 df-plt 15242 df-lub 15258 df-glb 15259 df-join 15260 df-meet 15261 df-p0 15323 df-p1 15324 df-lat 15330 df-clat 15392 df-mnd 15529 df-submnd 15579 df-grp 15659 df-minusg 15660 df-sbg 15661 df-subg 15792 df-cntz 15949 df-oppg 15975 df-lsm 16251 df-cmn 16395 df-abl 16396 df-mgp 16709 df-ur 16721 df-rng 16765 df-oppr 16833 df-dvdsr 16851 df-unit 16852 df-invr 16882 df-dvr 16893 df-drng 16952 df-lmod 17068 df-lss 17132 df-lsp 17171 df-lvec 17302 df-lsatoms 32940 df-lshyp 32941 df-lcv 32983 df-lfl 33022 df-lkr 33050 df-ldual 33088 df-oposet 33140 df-ol 33142 df-oml 33143 df-covers 33230 df-ats 33231 df-atl 33262 df-cvlat 33286 df-hlat 33315 df-llines 33461 df-lplanes 33462 df-lvols 33463 df-lines 33464 df-psubsp 33466 df-pmap 33467 df-padd 33759 df-lhyp 33951 df-laut 33952 df-ldil 34067 df-ltrn 34068 df-trl 34122 df-tgrp 34706 df-tendo 34718 df-edring 34720 df-dveca 34966 df-disoa 34993 df-dvech 35043 df-dib 35103 df-dic 35137 df-dih 35193 df-doch 35312 df-djh 35359 df-lcdual 35551 df-mapd 35589 df-hdmap1 35758 |
This theorem is referenced by: hdmap1l6g 35781 |
Copyright terms: Public domain | W3C validator |