Description: Lemma for lcfr . (Contributed by NM, 11-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcfrlem17.h | |
|
lcfrlem17.o | |
||
lcfrlem17.u | |
||
lcfrlem17.v | |
||
lcfrlem17.p | |
||
lcfrlem17.z | |
||
lcfrlem17.n | |
||
lcfrlem17.a | |
||
lcfrlem17.k | |
||
lcfrlem17.x | |
||
lcfrlem17.y | |
||
lcfrlem17.ne | |
||
lcfrlem20.e | |
||
Assertion | lcfrlem20 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem17.h | |
|
2 | lcfrlem17.o | |
|
3 | lcfrlem17.u | |
|
4 | lcfrlem17.v | |
|
5 | lcfrlem17.p | |
|
6 | lcfrlem17.z | |
|
7 | lcfrlem17.n | |
|
8 | lcfrlem17.a | |
|
9 | lcfrlem17.k | |
|
10 | lcfrlem17.x | |
|
11 | lcfrlem17.y | |
|
12 | lcfrlem17.ne | |
|
13 | lcfrlem20.e | |
|
14 | eqid | |
|
15 | 1 3 9 | dvhlmod | |
16 | 10 | eldifad | |
17 | 11 | eldifad | |
18 | 4 7 14 15 16 17 | lsmpr | |
19 | 18 | ineq1d | |
20 | eqid | |
|
21 | eqid | |
|
22 | 1 3 9 | dvhlvec | |
23 | 1 2 3 4 5 6 7 8 9 10 11 12 | lcfrlem17 | |
24 | 1 2 3 4 6 21 9 23 | dochsnshp | |
25 | 4 7 6 8 15 10 | lsatlspsn | |
26 | 4 7 6 8 15 11 | lsatlspsn | |
27 | 4 5 | lmodvacl | |
28 | 15 16 17 27 | syl3anc | |
29 | 28 | snssd | |
30 | 1 3 4 20 2 | dochlss | |
31 | 9 29 30 | syl2anc | |
32 | 4 20 7 15 31 16 | lspsnel5 | |
33 | 13 32 | mtbid | |
34 | 20 14 21 8 22 24 25 26 12 33 | lshpat | |
35 | 19 34 | eqeltrd | |