Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 3-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hdmap14lem8.h | |
|
hdmap14lem8.u | |
||
hdmap14lem8.v | |
||
hdmap14lem8.q | |
||
hdmap14lem8.t | |
||
hdmap14lem8.o | |
||
hdmap14lem8.n | |
||
hdmap14lem8.r | |
||
hdmap14lem8.b | |
||
hdmap14lem8.c | |
||
hdmap14lem8.d | |
||
hdmap14lem8.e | |
||
hdmap14lem8.p | |
||
hdmap14lem8.a | |
||
hdmap14lem8.s | |
||
hdmap14lem8.k | |
||
hdmap14lem8.x | |
||
hdmap14lem8.y | |
||
hdmap14lem8.f | |
||
hdmap14lem8.g | |
||
hdmap14lem8.i | |
||
hdmap14lem8.xx | |
||
hdmap14lem8.yy | |
||
hdmap14lem8.ne | |
||
Assertion | hdmap14lem10 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmap14lem8.h | |
|
2 | hdmap14lem8.u | |
|
3 | hdmap14lem8.v | |
|
4 | hdmap14lem8.q | |
|
5 | hdmap14lem8.t | |
|
6 | hdmap14lem8.o | |
|
7 | hdmap14lem8.n | |
|
8 | hdmap14lem8.r | |
|
9 | hdmap14lem8.b | |
|
10 | hdmap14lem8.c | |
|
11 | hdmap14lem8.d | |
|
12 | hdmap14lem8.e | |
|
13 | hdmap14lem8.p | |
|
14 | hdmap14lem8.a | |
|
15 | hdmap14lem8.s | |
|
16 | hdmap14lem8.k | |
|
17 | hdmap14lem8.x | |
|
18 | hdmap14lem8.y | |
|
19 | hdmap14lem8.f | |
|
20 | hdmap14lem8.g | |
|
21 | hdmap14lem8.i | |
|
22 | hdmap14lem8.xx | |
|
23 | hdmap14lem8.yy | |
|
24 | hdmap14lem8.ne | |
|
25 | eqid | |
|
26 | 1 2 16 | dvhlmod | |
27 | 17 | eldifad | |
28 | 18 | eldifad | |
29 | 3 4 | lmodvacl | |
30 | 26 27 28 29 | syl3anc | |
31 | 1 2 3 5 8 9 10 12 25 13 14 15 16 30 19 | hdmap14lem2a | |
32 | 16 | 3ad2ant1 | |
33 | 17 | 3ad2ant1 | |
34 | 18 | 3ad2ant1 | |
35 | 19 | 3ad2ant1 | |
36 | 20 | 3ad2ant1 | |
37 | 21 | 3ad2ant1 | |
38 | 22 | 3ad2ant1 | |
39 | 23 | 3ad2ant1 | |
40 | 24 | 3ad2ant1 | |
41 | simp2 | |
|
42 | simp3 | |
|
43 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41 42 | hdmap14lem9 | |
44 | 43 | rexlimdv3a | |
45 | 31 44 | mpd | |