Step | Hyp | Ref
| Expression |
1 | | pm2mpval.p |
. . 3
Poly1 |
2 | | pm2mpval.c |
. . 3
Mat |
3 | | pm2mpval.b |
. . 3
|
4 | | pm2mpval.m |
. . 3
|
5 | | pm2mpval.e |
. . 3
.gmulGrp |
6 | | pm2mpval.x |
. . 3
var1 |
7 | | pm2mpval.a |
. . 3
Mat |
8 | | pm2mpval.q |
. . 3
Poly1 |
9 | | pm2mpval.t |
. . 3
pMatToMatPoly |
10 | | pm2mpcl.l |
. . 3
|
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pm2mpf 20603 |
. 2
|
12 | 7 | matring 20249 |
. . . . . 6
|
13 | 12 | adantr 481 |
. . . . 5
|
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pm2mpcl 20602 |
. . . . . . 7
|
15 | 14 | 3expa 1265 |
. . . . . 6
|
16 | 15 | adantrr 753 |
. . . . 5
|
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pm2mpcl 20602 |
. . . . . . . 8
|
18 | 17 | 3expia 1267 |
. . . . . . 7
|
19 | 18 | adantld 483 |
. . . . . 6
|
20 | 19 | imp 445 |
. . . . 5
|
21 | | eqid 2622 |
. . . . . . 7
coe1 coe1 |
22 | | eqid 2622 |
. . . . . . 7
coe1 coe1 |
23 | 8, 10, 21, 22 | ply1coe1eq 19668 |
. . . . . 6
coe1 coe1
|
24 | 23 | bicomd 213 |
. . . . 5
coe1 coe1 |
25 | 13, 16, 20, 24 | syl3anc 1326 |
. . . 4
coe1 coe1 |
26 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
|
27 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
28 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pm2mpfval 20601 |
. . . . . . . . . . . . . . . . . 18
g
decompPMat
|
30 | 26, 27, 28, 29 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
g
decompPMat
|
31 | 30 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
g decompPMat |
32 | 31 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
coe1 coe1 g
decompPMat
|
33 | 32 | fveq1d 6193 |
. . . . . . . . . . . . . 14
coe1 coe1 g
decompPMat
|
34 | | simplll 798 |
. . . . . . . . . . . . . . 15
|
35 | 28 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | anim1i 592 |
. . . . . . . . . . . . . . 15
|
37 | 1, 2, 3, 4, 5, 6, 7, 8 | pm2mpf1lem 20599 |
. . . . . . . . . . . . . . 15
coe1 g
decompPMat
decompPMat
|
38 | 34, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . . 14
coe1 g
decompPMat
decompPMat
|
39 | 33, 38 | eqtrd 2656 |
. . . . . . . . . . . . 13
coe1 decompPMat |
40 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
41 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pm2mpfval 20601 |
. . . . . . . . . . . . . . . . . 18
g
decompPMat
|
42 | 26, 27, 40, 41 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
g
decompPMat
|
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
coe1 coe1 g decompPMat |
44 | 43 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
coe1 coe1 g
decompPMat
|
45 | 44 | ad2antrr 762 |
. . . . . . . . . . . . . 14
coe1 coe1 g
decompPMat
|
46 | 40 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | anim1i 592 |
. . . . . . . . . . . . . . 15
|
48 | 1, 2, 3, 4, 5, 6, 7, 8 | pm2mpf1lem 20599 |
. . . . . . . . . . . . . . 15
coe1 g
decompPMat
decompPMat
|
49 | 34, 47, 48 | syl2anc 693 |
. . . . . . . . . . . . . 14
coe1 g
decompPMat
decompPMat
|
50 | 45, 49 | eqtrd 2656 |
. . . . . . . . . . . . 13
coe1 decompPMat |
51 | 39, 50 | eqeq12d 2637 |
. . . . . . . . . . . 12
coe1 coe1 decompPMat decompPMat |
52 | 2, 3 | decpmatval 20570 |
. . . . . . . . . . . . . . . . 17
decompPMat
coe1 |
53 | 28, 52 | sylan 488 |
. . . . . . . . . . . . . . . 16
decompPMat
coe1 |
54 | 2, 3 | decpmatval 20570 |
. . . . . . . . . . . . . . . . 17
decompPMat
coe1 |
55 | 40, 54 | sylan 488 |
. . . . . . . . . . . . . . . 16
decompPMat
coe1 |
56 | 53, 55 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
decompPMat decompPMat
coe1
coe1 |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
58 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
59 | | simplll 798 |
. . . . . . . . . . . . . . . . 17
|
60 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
|
61 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
62 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . 19
|
63 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 3 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | 64 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 66 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | 67 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 68, 3 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 2, 61, 3, 62, 63, 69 | matecld 20232 |
. . . . . . . . . . . . . . . . . 18
|
71 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . 18
|
72 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 |
73 | 72, 61, 1, 57 | coe1fvalcl 19582 |
. . . . . . . . . . . . . . . . . 18
coe1 |
74 | 70, 71, 73 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
coe1 |
75 | 7, 57, 58, 59, 60, 74 | matbas2d 20229 |
. . . . . . . . . . . . . . . 16
coe1 |
76 | 3 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | 76 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
78 | 77 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 80, 3 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 2, 61, 3, 62, 63, 81 | matecld 20232 |
. . . . . . . . . . . . . . . . . 18
|
83 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 |
84 | 83, 61, 1, 57 | coe1fvalcl 19582 |
. . . . . . . . . . . . . . . . . 18
coe1 |
85 | 82, 71, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
coe1 |
86 | 7, 57, 58, 59, 60, 85 | matbas2d 20229 |
. . . . . . . . . . . . . . . 16
coe1 |
87 | 7, 58 | eqmat 20230 |
. . . . . . . . . . . . . . . 16
coe1
coe1 coe1 coe1
coe1
coe1 |
88 | 75, 86, 87 | syl2anc 693 |
. . . . . . . . . . . . . . 15
coe1 coe1
coe1
coe1 |
89 | 56, 88 | bitrd 268 |
. . . . . . . . . . . . . 14
decompPMat decompPMat
coe1 coe1 |
90 | 89 | adantlr 751 |
. . . . . . . . . . . . 13
decompPMat decompPMat
coe1 coe1 |
91 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1 |
92 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1 |
93 | 91, 92 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
coe1 coe1 coe1
coe1 |
94 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1 |
95 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1 |
96 | 94, 95 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
coe1 coe1 coe1
coe1 |
97 | 93, 96 | rspc2va 3323 |
. . . . . . . . . . . . . . . . . . 19
coe1
coe1 coe1 coe1 |
98 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1
coe1 |
99 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
coe1 coe1 |
101 | 100 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
coe1 coe1 |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1 |
103 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
104 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
105 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 |
106 | 98, 102, 103, 104, 105 | ovmpt2d 6788 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1 |
107 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1
coe1 |
108 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
109 | 108 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
coe1 coe1 |
110 | 109 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
coe1 coe1 |
111 | 110 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1 |
112 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 |
113 | 107, 111,
103, 104, 112 | ovmpt2d 6788 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1 |
114 | 106, 113 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1
coe1 coe1 coe1 |
115 | 114 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . 21
coe1
coe1
coe1 coe1 |
116 | 115 | exp31 630 |
. . . . . . . . . . . . . . . . . . . 20
coe1 coe1 coe1 coe1 |
117 | 116 | com14 96 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1
coe1 coe1 |
118 | 97, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
coe1
coe1
coe1 coe1 |
119 | 118 | ex 450 |
. . . . . . . . . . . . . . . . 17
coe1
coe1
coe1 coe1 |
120 | 119 | com25 99 |
. . . . . . . . . . . . . . . 16
coe1
coe1
coe1 coe1 |
121 | 120 | pm2.43i 52 |
. . . . . . . . . . . . . . 15
coe1 coe1 coe1 coe1 |
122 | 121 | impcom 446 |
. . . . . . . . . . . . . 14
coe1 coe1
coe1 coe1 |
123 | 122 | imp 445 |
. . . . . . . . . . . . 13
coe1
coe1
coe1 coe1 |
124 | 90, 123 | sylbid 230 |
. . . . . . . . . . . 12
decompPMat decompPMat coe1 coe1 |
125 | 51, 124 | sylbid 230 |
. . . . . . . . . . 11
coe1 coe1 coe1 coe1 |
126 | 125 | ralimdva 2962 |
. . . . . . . . . 10
coe1 coe1 coe1 coe1 |
127 | 126 | impancom 456 |
. . . . . . . . 9
coe1 coe1 coe1 coe1 |
128 | 127 | imp 445 |
. . . . . . . 8
coe1 coe1
coe1 coe1 |
129 | 27 | ad2antrr 762 |
. . . . . . . . 9
coe1 coe1
|
130 | | simprl 794 |
. . . . . . . . . 10
coe1 coe1
|
131 | | simprr 796 |
. . . . . . . . . 10
coe1 coe1
|
132 | 66 | ad2antlr 763 |
. . . . . . . . . . . 12
coe1 coe1
|
133 | 132 | adantr 481 |
. . . . . . . . . . 11
coe1 coe1
|
134 | 133, 3 | syl6eleqr 2712 |
. . . . . . . . . 10
coe1 coe1
|
135 | 2, 61, 3, 130, 131, 134 | matecld 20232 |
. . . . . . . . 9
coe1 coe1
|
136 | 78 | ad2antrr 762 |
. . . . . . . . . . 11
coe1 coe1
|
137 | 136, 3 | syl6eleqr 2712 |
. . . . . . . . . 10
coe1 coe1
|
138 | 2, 61, 3, 130, 131, 137 | matecld 20232 |
. . . . . . . . 9
coe1 coe1
|
139 | | eqid 2622 |
. . . . . . . . . . 11
coe1 coe1 |
140 | | eqid 2622 |
. . . . . . . . . . 11
coe1 coe1 |
141 | 1, 61, 139, 140 | ply1coe1eq 19668 |
. . . . . . . . . 10
coe1 coe1
|
142 | 141 | bicomd 213 |
. . . . . . . . 9
coe1 coe1 |
143 | 129, 135,
138, 142 | syl3anc 1326 |
. . . . . . . 8
coe1 coe1
coe1 coe1 |
144 | 128, 143 | mpbird 247 |
. . . . . . 7
coe1 coe1
|
145 | 144 | ralrimivva 2971 |
. . . . . 6
coe1 coe1
|
146 | 2, 3 | eqmat 20230 |
. . . . . . 7
|
147 | 146 | ad2antlr 763 |
. . . . . 6
coe1 coe1
|
148 | 145, 147 | mpbird 247 |
. . . . 5
coe1 coe1
|
149 | 148 | ex 450 |
. . . 4
coe1 coe1 |
150 | 25, 149 | sylbid 230 |
. . 3
|
151 | 150 | ralrimivva 2971 |
. 2
|
152 | | dff13 6512 |
. 2
|
153 | 11, 151, 152 | sylanbrc 698 |
1
|