Step | Hyp | Ref
| Expression |
1 | | pm2mpfo.b |
. 2
|
2 | | pm2mpfo.l |
. 2
|
3 | | eqid 2622 |
. 2
|
4 | | eqid 2622 |
. 2
|
5 | | pm2mpfo.p |
. . . 4
Poly1 |
6 | | pm2mpfo.c |
. . . 4
Mat |
7 | 5, 6 | pmatring 20498 |
. . 3
|
8 | | ringgrp 18552 |
. . 3
|
9 | 7, 8 | syl 17 |
. 2
|
10 | | pm2mpfo.a |
. . . . 5
Mat |
11 | 10 | matring 20249 |
. . . 4
|
12 | | pm2mpfo.q |
. . . . 5
Poly1 |
13 | 12 | ply1ring 19618 |
. . . 4
|
14 | 11, 13 | syl 17 |
. . 3
|
15 | | ringgrp 18552 |
. . 3
|
16 | 14, 15 | syl 17 |
. 2
|
17 | | pm2mpfo.m |
. . 3
|
18 | | pm2mpfo.e |
. . 3
.gmulGrp |
19 | | pm2mpfo.x |
. . 3
var1 |
20 | | pm2mpfo.t |
. . 3
pMatToMatPoly |
21 | 5, 6, 1, 17, 18, 19, 10, 12, 20, 2 | pm2mpf 20603 |
. 2
|
22 | | ringmnd 18556 |
. . . . . . . . . . . . . 14
|
23 | 7, 22 | syl 17 |
. . . . . . . . . . . . 13
|
24 | 23 | anim1i 592 |
. . . . . . . . . . . 12
|
25 | | 3anass 1042 |
. . . . . . . . . . . 12
|
26 | 24, 25 | sylibr 224 |
. . . . . . . . . . 11
|
27 | 1, 3 | mndcl 17301 |
. . . . . . . . . . 11
|
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
|
29 | 6, 1 | decpmatval 20570 |
. . . . . . . . . 10
decompPMat coe1 |
30 | 28, 29 | sylan 488 |
. . . . . . . . 9
decompPMat
coe1 |
31 | | simplll 798 |
. . . . . . . . . . 11
|
32 | | fvexd 6203 |
. . . . . . . . . . 11
coe1 |
33 | | fvexd 6203 |
. . . . . . . . . . 11
coe1 |
34 | | eqidd 2623 |
. . . . . . . . . . 11
coe1
coe1 |
35 | | eqidd 2623 |
. . . . . . . . . . 11
coe1
coe1 |
36 | 31, 31, 32, 33, 34, 35 | offval22 7253 |
. . . . . . . . . 10
coe1
coe1 coe1 coe1 |
37 | | eqid 2622 |
. . . . . . . . . . . 12
|
38 | | eqid 2622 |
. . . . . . . . . . . 12
|
39 | | simpllr 799 |
. . . . . . . . . . . 12
|
40 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
41 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
42 | 1 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 42 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
45 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 6, 45 | matecl 20231 |
. . . . . . . . . . . . . . . . . 18
|
47 | 40, 41, 44, 46 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | ex 450 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | adantrr 753 |
. . . . . . . . . . . . . . 15
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . . 14
|
51 | 50 | 3impib 1262 |
. . . . . . . . . . . . 13
|
52 | | simpr 477 |
. . . . . . . . . . . . . 14
|
53 | 52 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
54 | | eqid 2622 |
. . . . . . . . . . . . . 14
coe1 coe1 |
55 | 54, 45, 5, 37 | coe1fvalcl 19582 |
. . . . . . . . . . . . 13
coe1 |
56 | 51, 53, 55 | syl2anc 693 |
. . . . . . . . . . . 12
coe1 |
57 | 10, 37, 38, 31, 39, 56 | matbas2d 20229 |
. . . . . . . . . . 11
coe1 |
58 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
59 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
60 | 1 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | 60 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
63 | 6, 45 | matecl 20231 |
. . . . . . . . . . . . . . . . . 18
|
64 | 58, 59, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | ex 450 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | adantrl 752 |
. . . . . . . . . . . . . . 15
|
67 | 66 | adantr 481 |
. . . . . . . . . . . . . 14
|
68 | 67 | 3impib 1262 |
. . . . . . . . . . . . 13
|
69 | | eqid 2622 |
. . . . . . . . . . . . . 14
coe1 coe1 |
70 | 69, 45, 5, 37 | coe1fvalcl 19582 |
. . . . . . . . . . . . 13
coe1 |
71 | 68, 53, 70 | syl2anc 693 |
. . . . . . . . . . . 12
coe1 |
72 | 10, 37, 38, 31, 39, 71 | matbas2d 20229 |
. . . . . . . . . . 11
coe1 |
73 | | eqid 2622 |
. . . . . . . . . . . 12
|
74 | | eqid 2622 |
. . . . . . . . . . . 12
|
75 | 10, 38, 73, 74 | matplusg2 20233 |
. . . . . . . . . . 11
coe1
coe1 coe1 coe1
coe1 coe1 |
76 | 57, 72, 75 | syl2anc 693 |
. . . . . . . . . 10
coe1 coe1
coe1 coe1 |
77 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | anim1i 592 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | 3impb 1260 |
. . . . . . . . . . . . . . 15
|
80 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
81 | 6, 1, 3, 80 | matplusgcell 20239 |
. . . . . . . . . . . . . . 15
|
82 | 79, 81 | syl 17 |
. . . . . . . . . . . . . 14
|
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . 13
coe1 coe1 |
84 | 83 | fveq1d 6193 |
. . . . . . . . . . . 12
coe1 coe1 |
85 | 39 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
86 | 5, 45, 80, 74 | coe1addfv 19635 |
. . . . . . . . . . . . 13
coe1 coe1 coe1 |
87 | 85, 51, 68, 53, 86 | syl31anc 1329 |
. . . . . . . . . . . 12
coe1 coe1 coe1 |
88 | 84, 87 | eqtrd 2656 |
. . . . . . . . . . 11
coe1 coe1 coe1 |
89 | 88 | mpt2eq3dva 6719 |
. . . . . . . . . 10
coe1 coe1 coe1 |
90 | 36, 76, 89 | 3eqtr4rd 2667 |
. . . . . . . . 9
coe1
coe1
coe1 |
91 | 12 | ply1sca 19623 |
. . . . . . . . . . . . 13
Scalar |
92 | 11, 91 | syl 17 |
. . . . . . . . . . . 12
Scalar |
93 | 92 | ad2antrr 762 |
. . . . . . . . . . 11
Scalar |
94 | 93 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
95 | | simprl 794 |
. . . . . . . . . . . 12
|
96 | 6, 1 | decpmatval 20570 |
. . . . . . . . . . . 12
decompPMat
coe1 |
97 | 95, 96 | sylan 488 |
. . . . . . . . . . 11
decompPMat
coe1 |
98 | 97 | eqcomd 2628 |
. . . . . . . . . 10
coe1 decompPMat
|
99 | | simprr 796 |
. . . . . . . . . . . 12
|
100 | 6, 1 | decpmatval 20570 |
. . . . . . . . . . . 12
decompPMat
coe1 |
101 | 99, 100 | sylan 488 |
. . . . . . . . . . 11
decompPMat
coe1 |
102 | 101 | eqcomd 2628 |
. . . . . . . . . 10
coe1 decompPMat
|
103 | 94, 98, 102 | oveq123d 6671 |
. . . . . . . . 9
coe1 coe1 decompPMat
Scalar decompPMat |
104 | 30, 90, 103 | 3eqtrd 2660 |
. . . . . . . 8
decompPMat
decompPMat Scalar decompPMat |
105 | 104 | oveq1d 6665 |
. . . . . . 7
decompPMat decompPMat Scalar decompPMat
|
106 | 12 | ply1lmod 19622 |
. . . . . . . . . 10
|
107 | 11, 106 | syl 17 |
. . . . . . . . 9
|
108 | 107 | ad2antrr 762 |
. . . . . . . 8
|
109 | | simpl 473 |
. . . . . . . . . . 11
|
110 | 109 | ad2antlr 763 |
. . . . . . . . . 10
|
111 | 5, 6, 1, 10, 38 | decpmatcl 20572 |
. . . . . . . . . 10
decompPMat |
112 | 39, 110, 52, 111 | syl3anc 1326 |
. . . . . . . . 9
decompPMat
|
113 | 92 | eqcomd 2628 |
. . . . . . . . . . 11
Scalar |
114 | 113 | ad2antrr 762 |
. . . . . . . . . 10
Scalar |
115 | 114 | fveq2d 6195 |
. . . . . . . . 9
Scalar |
116 | 112, 115 | eleqtrrd 2704 |
. . . . . . . 8
decompPMat
Scalar |
117 | | simpr 477 |
. . . . . . . . . . 11
|
118 | 117 | ad2antlr 763 |
. . . . . . . . . 10
|
119 | 5, 6, 1, 10, 38 | decpmatcl 20572 |
. . . . . . . . . 10
decompPMat |
120 | 39, 118, 52, 119 | syl3anc 1326 |
. . . . . . . . 9
decompPMat
|
121 | 120, 115 | eleqtrrd 2704 |
. . . . . . . 8
decompPMat
Scalar |
122 | | eqid 2622 |
. . . . . . . . . . . 12
mulGrp mulGrp |
123 | 122 | ringmgp 18553 |
. . . . . . . . . . 11
mulGrp |
124 | 14, 123 | syl 17 |
. . . . . . . . . 10
mulGrp |
125 | 124 | ad2antrr 762 |
. . . . . . . . 9
mulGrp |
126 | 19, 12, 2 | vr1cl 19587 |
. . . . . . . . . . 11
|
127 | 11, 126 | syl 17 |
. . . . . . . . . 10
|
128 | 127 | ad2antrr 762 |
. . . . . . . . 9
|
129 | 122, 2 | mgpbas 18495 |
. . . . . . . . . 10
mulGrp |
130 | 129, 18 | mulgnn0cl 17558 |
. . . . . . . . 9
mulGrp
|
131 | 125, 52, 128, 130 | syl3anc 1326 |
. . . . . . . 8
|
132 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
133 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
134 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
135 | 2, 4, 132, 17, 133, 134 | lmodvsdir 18887 |
. . . . . . . 8
decompPMat
Scalar
decompPMat Scalar
decompPMat
Scalar decompPMat decompPMat decompPMat
|
136 | 108, 116,
121, 131, 135 | syl13anc 1328 |
. . . . . . 7
decompPMat Scalar decompPMat
decompPMat
decompPMat
|
137 | 105, 136 | eqtrd 2656 |
. . . . . 6
decompPMat decompPMat
decompPMat
|
138 | 137 | mpteq2dva 4744 |
. . . . 5
decompPMat
decompPMat
decompPMat
|
139 | 138 | oveq2d 6666 |
. . . 4
g decompPMat g decompPMat
decompPMat
|
140 | | eqid 2622 |
. . . . 5
|
141 | | ringcmn 18581 |
. . . . . . 7
CMnd |
142 | 14, 141 | syl 17 |
. . . . . 6
CMnd |
143 | 142 | adantr 481 |
. . . . 5
CMnd |
144 | | nn0ex 11298 |
. . . . . 6
|
145 | 144 | a1i 11 |
. . . . 5
|
146 | 109 | anim2i 593 |
. . . . . . 7
|
147 | | df-3an 1039 |
. . . . . . 7
|
148 | 146, 147 | sylibr 224 |
. . . . . 6
|
149 | 5, 6, 1, 17, 18, 19, 10, 12, 2 | pm2mpghmlem1 20618 |
. . . . . 6
decompPMat
|
150 | 148, 149 | sylan 488 |
. . . . 5
decompPMat |
151 | 117 | anim2i 593 |
. . . . . . 7
|
152 | | df-3an 1039 |
. . . . . . 7
|
153 | 151, 152 | sylibr 224 |
. . . . . 6
|
154 | 5, 6, 1, 17, 18, 19, 10, 12, 2 | pm2mpghmlem1 20618 |
. . . . . 6
decompPMat
|
155 | 153, 154 | sylan 488 |
. . . . 5
decompPMat |
156 | | eqidd 2623 |
. . . . 5
decompPMat
decompPMat
|
157 | | eqidd 2623 |
. . . . 5
decompPMat
decompPMat
|
158 | 5, 6, 1, 17, 18, 19, 10, 12 | pm2mpghmlem2 20617 |
. . . . . 6
decompPMat
finSupp
|
159 | 148, 158 | syl 17 |
. . . . 5
decompPMat
finSupp
|
160 | 5, 6, 1, 17, 18, 19, 10, 12 | pm2mpghmlem2 20617 |
. . . . . 6
decompPMat
finSupp
|
161 | 153, 160 | syl 17 |
. . . . 5
decompPMat
finSupp
|
162 | 2, 140, 4, 143, 145, 150, 155, 156, 157, 159, 161 | gsummptfsadd 18324 |
. . . 4
g decompPMat
decompPMat
g decompPMat g decompPMat |
163 | 139, 162 | eqtrd 2656 |
. . 3
g decompPMat g decompPMat g decompPMat |
164 | | simpll 790 |
. . . 4
|
165 | | simplr 792 |
. . . 4
|
166 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 20601 |
. . . 4
g decompPMat |
167 | 164, 165,
28, 166 | syl3anc 1326 |
. . 3
g decompPMat |
168 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 20601 |
. . . . 5
g
decompPMat
|
169 | 164, 165,
95, 168 | syl3anc 1326 |
. . . 4
g
decompPMat
|
170 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 20601 |
. . . . 5
g
decompPMat
|
171 | 164, 165,
99, 170 | syl3anc 1326 |
. . . 4
g
decompPMat
|
172 | 169, 171 | oveq12d 6668 |
. . 3
g
decompPMat
g decompPMat |
173 | 163, 167,
172 | 3eqtr4d 2666 |
. 2
|
174 | 1, 2, 3, 4, 9, 16,
21, 173 | isghmd 17669 |
1
|