Description: Lemma for cayhamlem3 . (Contributed by AV, 24-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cayhamlem2.k | |
|
cayhamlem2.a | |
||
cayhamlem2.b | |
||
cayhamlem2.1 | |
||
cayhamlem2.m | |
||
cayhamlem2.e | |
||
cayhamlem2.r | |
||
Assertion | cayhamlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cayhamlem2.k | |
|
2 | cayhamlem2.a | |
|
3 | cayhamlem2.b | |
|
4 | cayhamlem2.1 | |
|
5 | cayhamlem2.m | |
|
6 | cayhamlem2.e | |
|
7 | cayhamlem2.r | |
|
8 | elmapi | |
|
9 | 8 | ffvelcdmda | |
10 | 9 | adantl | |
11 | 2 | matsca2 | |
12 | 11 | 3adant3 | |
13 | 12 | fveq2d | |
14 | 1 13 | eqtr2id | |
15 | 14 | eleq2d | |
16 | 15 | adantr | |
17 | 10 16 | mpbird | |
18 | eqid | |
|
19 | eqid | |
|
20 | eqid | |
|
21 | 18 19 20 5 4 | asclval | |
22 | 17 21 | syl | |
23 | 22 | eqcomd | |
24 | 23 | oveq2d | |
25 | 2 | matassa | |
26 | 25 | 3adant3 | |
27 | 26 | adantr | |
28 | eqid | |
|
29 | 28 3 | mgpbas | |
30 | crngring | |
|
31 | 30 | anim2i | |
32 | 31 | 3adant3 | |
33 | 2 | matring | |
34 | 28 | ringmgp | |
35 | 32 33 34 | 3syl | |
36 | 35 | adantr | |
37 | simprr | |
|
38 | simpl3 | |
|
39 | 29 6 36 37 38 | mulgnn0cld | |
40 | 18 19 20 3 7 5 | asclmul2 | |
41 | 27 17 39 40 | syl3anc | |
42 | 24 41 | eqtr2d | |