Description: Lemma 1 for lincresunit3 . (Contributed by AV, 17-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lincresunit.b | |
|
lincresunit.r | |
||
lincresunit.e | |
||
lincresunit.u | |
||
lincresunit.0 | |
||
lincresunit.z | |
||
lincresunit.n | |
||
lincresunit.i | |
||
lincresunit.t | |
||
lincresunit.g | |
||
Assertion | lincresunit3lem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lincresunit.b | |
|
2 | lincresunit.r | |
|
3 | lincresunit.e | |
|
4 | lincresunit.u | |
|
5 | lincresunit.0 | |
|
6 | lincresunit.z | |
|
7 | lincresunit.n | |
|
8 | lincresunit.i | |
|
9 | lincresunit.t | |
|
10 | lincresunit.g | |
|
11 | fveq2 | |
|
12 | 11 | oveq2d | |
13 | simpr3 | |
|
14 | ovexd | |
|
15 | 10 12 13 14 | fvmptd3 | |
16 | 15 | oveq1d | |
17 | 16 | oveq2d | |
18 | simp2 | |
|
19 | 18 | adantr | |
20 | 2 | lmodfgrp | |
21 | 20 | 3ad2ant2 | |
22 | 3 4 | unitcl | |
23 | 22 | 3ad2ant2 | |
24 | 3 7 | grpinvcl | |
25 | 21 23 24 | syl2an | |
26 | 3simpa | |
|
27 | 26 | anim2i | |
28 | eldifi | |
|
29 | 28 | 3ad2ant3 | |
30 | 29 | adantl | |
31 | 1 2 3 4 5 6 7 8 9 10 | lincresunitlem2 | |
32 | 27 30 31 | syl2anc | |
33 | elpwi | |
|
34 | 33 | sseld | |
35 | 28 34 | syl5com | |
36 | 35 | 3ad2ant3 | |
37 | 36 | com12 | |
38 | 37 | 3ad2ant1 | |
39 | 38 | imp | |
40 | eqid | |
|
41 | 1 2 40 3 9 | lmodvsass | |
42 | 41 | eqcomd | |
43 | 19 25 32 39 42 | syl13anc | |
44 | 2 | lmodring | |
45 | 44 | 3ad2ant2 | |
46 | 45 | adantr | |
47 | elmapi | |
|
48 | ffvelrn | |
|
49 | 47 28 48 | syl2an | |
50 | 49 | 3adant2 | |
51 | 50 | adantl | |
52 | simp2 | |
|
53 | 52 | adantl | |
54 | 3 4 7 8 9 | invginvrid | |
55 | 46 51 53 54 | syl3anc | |
56 | 55 | oveq1d | |
57 | 17 43 56 | 3eqtrd | |