Step | Hyp | Ref
| Expression |
1 | | m2cpminvid2lem.s |
. . . . . . . 8
ConstPolyMat |
2 | | m2cpminvid2lem.p |
. . . . . . . 8
Poly1 |
3 | | eqid 2622 |
. . . . . . . 8
Mat Mat |
4 | | eqid 2622 |
. . . . . . . 8
Mat Mat |
5 | 1, 2, 3, 4 | cpmatelimp 20517 |
. . . . . . 7
Mat
coe1 |
6 | 5 | 3impia 1261 |
. . . . . 6
Mat
coe1 |
7 | | simpr 477 |
. . . . . 6
Mat
coe1
coe1 |
8 | 6, 7 | syl 17 |
. . . . 5
coe1 |
9 | 8 | adantr 481 |
. . . 4
coe1 |
10 | | oveq1 6657 |
. . . . . . . . . . 11
|
11 | 10 | fveq2d 6195 |
. . . . . . . . . 10
coe1 coe1 |
12 | 11 | fveq1d 6193 |
. . . . . . . . 9
coe1 coe1 |
13 | 12 | eqeq1d 2624 |
. . . . . . . 8
coe1 coe1 |
14 | 13 | ralbidv 2986 |
. . . . . . 7
coe1
coe1 |
15 | | oveq2 6658 |
. . . . . . . . . . 11
|
16 | 15 | fveq2d 6195 |
. . . . . . . . . 10
coe1 coe1 |
17 | 16 | fveq1d 6193 |
. . . . . . . . 9
coe1 coe1 |
18 | 17 | eqeq1d 2624 |
. . . . . . . 8
coe1 coe1 |
19 | 18 | ralbidv 2986 |
. . . . . . 7
coe1
coe1 |
20 | 14, 19 | rspc2v 3322 |
. . . . . 6
coe1 coe1 |
21 | 20 | adantl 482 |
. . . . 5
coe1 coe1 |
22 | | fveq2 6191 |
. . . . . . . 8
coe1 coe1 |
23 | 22 | eqeq1d 2624 |
. . . . . . 7
coe1 coe1 |
24 | 23 | cbvralv 3171 |
. . . . . 6
coe1
coe1 |
25 | | simpl2 1065 |
. . . . . . . . . . . . . . . . 17
|
26 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
27 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
28 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 1, 2, 3, 4 | cpmatpmat 20515 |
. . . . . . . . . . . . . . . . . . . 20
Mat |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Mat |
32 | 3, 26, 4, 27, 29, 31 | matecld 20232 |
. . . . . . . . . . . . . . . . . 18
|
33 | | 0nn0 11307 |
. . . . . . . . . . . . . . . . . 18
|
34 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 |
35 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 34, 26, 2, 35 | coe1fvalcl 19582 |
. . . . . . . . . . . . . . . . . 18
coe1 |
37 | 32, 33, 36 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
coe1 |
38 | 25, 37 | jca 554 |
. . . . . . . . . . . . . . . 16
coe1 |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
coe1 |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
algSc algSc |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
42 | 2, 40, 35, 41 | coe1scl 19657 |
. . . . . . . . . . . . . . 15
coe1
coe1algSccoe1 coe1 |
43 | 39, 42 | syl 17 |
. . . . . . . . . . . . . 14
coe1algSccoe1 coe1 |
44 | 43 | fveq1d 6193 |
. . . . . . . . . . . . 13
coe1algSccoe1 coe1 |
45 | | eqidd 2623 |
. . . . . . . . . . . . . 14
coe1 coe1 |
46 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | ifbid 4108 |
. . . . . . . . . . . . . . 15
coe1 coe1 |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . 14
coe1 coe1 |
49 | | nnnn0 11299 |
. . . . . . . . . . . . . . 15
|
50 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
|
51 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
coe1 |
52 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
53 | 51, 52 | ifex 4156 |
. . . . . . . . . . . . . . 15
coe1 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
coe1 |
55 | 45, 48, 50, 54 | fvmptd 6288 |
. . . . . . . . . . . . 13
coe1 coe1 |
56 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | neneqd 2799 |
. . . . . . . . . . . . . . 15
|
58 | 57 | adantl 482 |
. . . . . . . . . . . . . 14
|
59 | 58 | iffalsed 4097 |
. . . . . . . . . . . . 13
coe1 |
60 | 44, 55, 59 | 3eqtrd 2660 |
. . . . . . . . . . . 12
coe1algSccoe1 |
61 | | eqcom 2629 |
. . . . . . . . . . . . 13
coe1 coe1 |
62 | 61 | biimpi 206 |
. . . . . . . . . . . 12
coe1 coe1 |
63 | 60, 62 | sylan9eq 2676 |
. . . . . . . . . . 11
coe1
coe1algSccoe1 coe1 |
64 | 63 | ex 450 |
. . . . . . . . . 10
coe1 coe1algSccoe1 coe1 |
65 | 64 | ralimdva 2962 |
. . . . . . . . 9
coe1 coe1algSccoe1 coe1 |
66 | 65 | imp 445 |
. . . . . . . 8
coe1
coe1algSccoe1 coe1 |
67 | 38 | adantr 481 |
. . . . . . . . 9
coe1
coe1 |
68 | 2, 40, 35 | ply1sclid 19658 |
. . . . . . . . . 10
coe1
coe1 coe1algSccoe1 |
69 | 68 | eqcomd 2628 |
. . . . . . . . 9
coe1
coe1algSccoe1 coe1 |
70 | 67, 69 | syl 17 |
. . . . . . . 8
coe1
coe1algSccoe1 coe1 |
71 | 66, 70 | jca 554 |
. . . . . . 7
coe1
coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
72 | 71 | ex 450 |
. . . . . 6
coe1 coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
73 | 24, 72 | syl5bi 232 |
. . . . 5
coe1 coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
74 | 21, 73 | syld 47 |
. . . 4
coe1 coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
75 | 9, 74 | mpd 15 |
. . 3
coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
76 | | c0ex 10034 |
. . . 4
|
77 | | fveq2 6191 |
. . . . . 6
coe1algSccoe1 coe1algSccoe1 |
78 | | fveq2 6191 |
. . . . . 6
coe1 coe1 |
79 | 77, 78 | eqeq12d 2637 |
. . . . 5
coe1algSccoe1 coe1
coe1algSccoe1 coe1 |
80 | 79 | ralunsn 4422 |
. . . 4
coe1algSccoe1 coe1
coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
81 | 76, 80 | mp1i 13 |
. . 3
coe1algSccoe1 coe1
coe1algSccoe1 coe1 coe1algSccoe1 coe1 |
82 | 75, 81 | mpbird 247 |
. 2
coe1algSccoe1 coe1 |
83 | | df-n0 11293 |
. . 3
|
84 | 83 | raleqi 3142 |
. 2
coe1algSccoe1 coe1
coe1algSccoe1 coe1 |
85 | 82, 84 | sylibr 224 |
1
coe1algSccoe1 coe1 |