Metamath Proof Explorer


Theorem mplcoe1

Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplcoe1.p P = I mPoly R
mplcoe1.d D = f 0 I | f -1 Fin
mplcoe1.z 0 ˙ = 0 R
mplcoe1.o 1 ˙ = 1 R
mplcoe1.i φ I W
mplcoe1.b B = Base P
mplcoe1.n · ˙ = P
mplcoe1.r φ R Ring
mplcoe1.x φ X B
Assertion mplcoe1 φ X = P k D X k · ˙ y D if y = k 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 mplcoe1.p P = I mPoly R
2 mplcoe1.d D = f 0 I | f -1 Fin
3 mplcoe1.z 0 ˙ = 0 R
4 mplcoe1.o 1 ˙ = 1 R
5 mplcoe1.i φ I W
6 mplcoe1.b B = Base P
7 mplcoe1.n · ˙ = P
8 mplcoe1.r φ R Ring
9 mplcoe1.x φ X B
10 eqid Base R = Base R
11 1 10 6 2 9 mplelf φ X : D Base R
12 11 feqmptd φ X = y D X y
13 iftrue y supp 0 ˙ X if y supp 0 ˙ X X y 0 ˙ = X y
14 13 adantl φ y D y supp 0 ˙ X if y supp 0 ˙ X X y 0 ˙ = X y
15 eldif y D supp 0 ˙ X y D ¬ y supp 0 ˙ X
16 ssidd φ X supp 0 ˙ X supp 0 ˙
17 ovex 0 I V
18 2 17 rabex2 D V
19 18 a1i φ D V
20 3 fvexi 0 ˙ V
21 20 a1i φ 0 ˙ V
22 11 16 19 21 suppssr φ y D supp 0 ˙ X X y = 0 ˙
23 22 ifeq2d φ y D supp 0 ˙ X if y supp 0 ˙ X X y X y = if y supp 0 ˙ X X y 0 ˙
24 ifid if y supp 0 ˙ X X y X y = X y
25 23 24 eqtr3di φ y D supp 0 ˙ X if y supp 0 ˙ X X y 0 ˙ = X y
26 15 25 sylan2br φ y D ¬ y supp 0 ˙ X if y supp 0 ˙ X X y 0 ˙ = X y
27 26 anassrs φ y D ¬ y supp 0 ˙ X if y supp 0 ˙ X X y 0 ˙ = X y
28 14 27 pm2.61dan φ y D if y supp 0 ˙ X X y 0 ˙ = X y
29 28 mpteq2dva φ y D if y supp 0 ˙ X X y 0 ˙ = y D X y
30 12 29 eqtr4d φ X = y D if y supp 0 ˙ X X y 0 ˙
31 suppssdm X supp 0 ˙ dom X
32 31 11 fssdm φ X supp 0 ˙ D
33 eqid I mPwSer R = I mPwSer R
34 eqid Base I mPwSer R = Base I mPwSer R
35 1 33 34 3 6 mplelbas X B X Base I mPwSer R finSupp 0 ˙ X
36 35 simprbi X B finSupp 0 ˙ X
37 9 36 syl φ finSupp 0 ˙ X
38 37 fsuppimpd φ X supp 0 ˙ Fin
39 sseq1 w = w D D
40 mpteq1 w = k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = k X k · ˙ y D if y = k 1 ˙ 0 ˙
41 mpt0 k X k · ˙ y D if y = k 1 ˙ 0 ˙ =
42 40 41 eqtrdi w = k w X k · ˙ y D if y = k 1 ˙ 0 ˙ =
43 42 oveq2d w = P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = P
44 eqid 0 P = 0 P
45 44 gsum0 P = 0 P
46 43 45 eqtrdi w = P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
47 noel ¬ y
48 eleq2 w = y w y
49 47 48 mtbiri w = ¬ y w
50 49 iffalsed w = if y w X y 0 ˙ = 0 ˙
51 50 mpteq2dv w = y D if y w X y 0 ˙ = y D 0 ˙
52 46 51 eqeq12d w = P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ 0 P = y D 0 ˙
53 39 52 imbi12d w = w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ D 0 P = y D 0 ˙
54 53 imbi2d w = φ w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ φ D 0 P = y D 0 ˙
55 sseq1 w = x w D x D
56 mpteq1 w = x k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = k x X k · ˙ y D if y = k 1 ˙ 0 ˙
57 56 oveq2d w = x P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = P k x X k · ˙ y D if y = k 1 ˙ 0 ˙
58 eleq2 w = x y w y x
59 58 ifbid w = x if y w X y 0 ˙ = if y x X y 0 ˙
60 59 mpteq2dv w = x y D if y w X y 0 ˙ = y D if y x X y 0 ˙
61 57 60 eqeq12d w = x P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙
62 55 61 imbi12d w = x w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙
63 62 imbi2d w = x φ w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ φ x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙
64 sseq1 w = x z w D x z D
65 mpteq1 w = x z k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = k x z X k · ˙ y D if y = k 1 ˙ 0 ˙
66 65 oveq2d w = x z P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙
67 eleq2 w = x z y w y x z
68 67 ifbid w = x z if y w X y 0 ˙ = if y x z X y 0 ˙
69 68 mpteq2dv w = x z y D if y w X y 0 ˙ = y D if y x z X y 0 ˙
70 66 69 eqeq12d w = x z P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
71 64 70 imbi12d w = x z w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
72 71 imbi2d w = x z φ w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ φ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
73 sseq1 w = X supp 0 ˙ w D X supp 0 ˙ D
74 mpteq1 w = X supp 0 ˙ k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = k supp 0 ˙ X X k · ˙ y D if y = k 1 ˙ 0 ˙
75 74 oveq2d w = X supp 0 ˙ P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙
76 eleq2 w = X supp 0 ˙ y w y supp 0 ˙ X
77 76 ifbid w = X supp 0 ˙ if y w X y 0 ˙ = if y supp 0 ˙ X X y 0 ˙
78 77 mpteq2dv w = X supp 0 ˙ y D if y w X y 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
79 75 78 eqeq12d w = X supp 0 ˙ P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
80 73 79 imbi12d w = X supp 0 ˙ w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ X supp 0 ˙ D P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
81 80 imbi2d w = X supp 0 ˙ φ w D P k w X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y w X y 0 ˙ φ X supp 0 ˙ D P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
82 ringgrp R Ring R Grp
83 8 82 syl φ R Grp
84 1 2 3 44 5 83 mpl0 φ 0 P = D × 0 ˙
85 fconstmpt D × 0 ˙ = y D 0 ˙
86 84 85 eqtrdi φ 0 P = y D 0 ˙
87 86 a1d φ D 0 P = y D 0 ˙
88 ssun1 x x z
89 sstr2 x x z x z D x D
90 88 89 ax-mp x z D x D
91 90 imim1i x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ x z D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙
92 oveq1 P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙ = y D if y x X y 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙
93 eqid + P = + P
94 1 5 8 mplringd φ P Ring
95 ringcmn P Ring P CMnd
96 94 95 syl φ P CMnd
97 96 adantr φ x Fin ¬ z x x z D P CMnd
98 simprll φ x Fin ¬ z x x z D x Fin
99 simprr φ x Fin ¬ z x x z D x z D
100 99 unssad φ x Fin ¬ z x x z D x D
101 100 sselda φ x Fin ¬ z x x z D k x k D
102 5 adantr φ k D I W
103 8 adantr φ k D R Ring
104 1 102 103 mpllmodd φ k D P LMod
105 11 ffvelcdmda φ k D X k Base R
106 1 5 8 mplsca φ R = Scalar P
107 106 adantr φ k D R = Scalar P
108 107 fveq2d φ k D Base R = Base Scalar P
109 105 108 eleqtrd φ k D X k Base Scalar P
110 simpr φ k D k D
111 1 6 3 4 2 102 103 110 mplmon φ k D y D if y = k 1 ˙ 0 ˙ B
112 eqid Scalar P = Scalar P
113 eqid Base Scalar P = Base Scalar P
114 6 112 7 113 lmodvscl P LMod X k Base Scalar P y D if y = k 1 ˙ 0 ˙ B X k · ˙ y D if y = k 1 ˙ 0 ˙ B
115 104 109 111 114 syl3anc φ k D X k · ˙ y D if y = k 1 ˙ 0 ˙ B
116 115 adantlr φ x Fin ¬ z x x z D k D X k · ˙ y D if y = k 1 ˙ 0 ˙ B
117 101 116 syldan φ x Fin ¬ z x x z D k x X k · ˙ y D if y = k 1 ˙ 0 ˙ B
118 vex z V
119 118 a1i φ x Fin ¬ z x x z D z V
120 simprlr φ x Fin ¬ z x x z D ¬ z x
121 1 5 8 mpllmodd φ P LMod
122 121 adantr φ x Fin ¬ z x x z D P LMod
123 11 adantr φ x Fin ¬ z x x z D X : D Base R
124 99 unssbd φ x Fin ¬ z x x z D z D
125 118 snss z D z D
126 124 125 sylibr φ x Fin ¬ z x x z D z D
127 123 126 ffvelcdmd φ x Fin ¬ z x x z D X z Base R
128 106 adantr φ x Fin ¬ z x x z D R = Scalar P
129 128 fveq2d φ x Fin ¬ z x x z D Base R = Base Scalar P
130 127 129 eleqtrd φ x Fin ¬ z x x z D X z Base Scalar P
131 5 adantr φ x Fin ¬ z x x z D I W
132 8 adantr φ x Fin ¬ z x x z D R Ring
133 1 6 3 4 2 131 132 126 mplmon φ x Fin ¬ z x x z D y D if y = z 1 ˙ 0 ˙ B
134 6 112 7 113 lmodvscl P LMod X z Base Scalar P y D if y = z 1 ˙ 0 ˙ B X z · ˙ y D if y = z 1 ˙ 0 ˙ B
135 122 130 133 134 syl3anc φ x Fin ¬ z x x z D X z · ˙ y D if y = z 1 ˙ 0 ˙ B
136 fveq2 k = z X k = X z
137 equequ2 k = z y = k y = z
138 137 ifbid k = z if y = k 1 ˙ 0 ˙ = if y = z 1 ˙ 0 ˙
139 138 mpteq2dv k = z y D if y = k 1 ˙ 0 ˙ = y D if y = z 1 ˙ 0 ˙
140 136 139 oveq12d k = z X k · ˙ y D if y = k 1 ˙ 0 ˙ = X z · ˙ y D if y = z 1 ˙ 0 ˙
141 6 93 97 98 117 119 120 135 140 gsumunsn φ x Fin ¬ z x x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙
142 eqid + R = + R
143 123 ffvelcdmda φ x Fin ¬ z x x z D y D X y Base R
144 10 3 ring0cl R Ring 0 ˙ Base R
145 8 144 syl φ 0 ˙ Base R
146 145 ad2antrr φ x Fin ¬ z x x z D y D 0 ˙ Base R
147 143 146 ifcld φ x Fin ¬ z x x z D y D if y x X y 0 ˙ Base R
148 147 fmpttd φ x Fin ¬ z x x z D y D if y x X y 0 ˙ : D Base R
149 fvex Base R V
150 149 18 elmap y D if y x X y 0 ˙ Base R D y D if y x X y 0 ˙ : D Base R
151 148 150 sylibr φ x Fin ¬ z x x z D y D if y x X y 0 ˙ Base R D
152 33 10 2 34 131 psrbas φ x Fin ¬ z x x z D Base I mPwSer R = Base R D
153 151 152 eleqtrrd φ x Fin ¬ z x x z D y D if y x X y 0 ˙ Base I mPwSer R
154 18 mptex y D if y x X y 0 ˙ V
155 funmpt Fun y D if y x X y 0 ˙
156 154 155 20 3pm3.2i y D if y x X y 0 ˙ V Fun y D if y x X y 0 ˙ 0 ˙ V
157 156 a1i φ x Fin ¬ z x x z D y D if y x X y 0 ˙ V Fun y D if y x X y 0 ˙ 0 ˙ V
158 eldifn y D x ¬ y x
159 158 adantl φ x Fin ¬ z x x z D y D x ¬ y x
160 159 iffalsed φ x Fin ¬ z x x z D y D x if y x X y 0 ˙ = 0 ˙
161 18 a1i φ x Fin ¬ z x x z D D V
162 160 161 suppss2 φ x Fin ¬ z x x z D y D if y x X y 0 ˙ supp 0 ˙ x
163 suppssfifsupp y D if y x X y 0 ˙ V Fun y D if y x X y 0 ˙ 0 ˙ V x Fin y D if y x X y 0 ˙ supp 0 ˙ x finSupp 0 ˙ y D if y x X y 0 ˙
164 157 98 162 163 syl12anc φ x Fin ¬ z x x z D finSupp 0 ˙ y D if y x X y 0 ˙
165 1 33 34 3 6 mplelbas y D if y x X y 0 ˙ B y D if y x X y 0 ˙ Base I mPwSer R finSupp 0 ˙ y D if y x X y 0 ˙
166 153 164 165 sylanbrc φ x Fin ¬ z x x z D y D if y x X y 0 ˙ B
167 1 6 142 93 166 135 mpladd φ x Fin ¬ z x x z D y D if y x X y 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙ = y D if y x X y 0 ˙ + R f X z · ˙ y D if y = z 1 ˙ 0 ˙
168 ovexd φ x Fin ¬ z x x z D y D X z R if y = z 1 ˙ 0 ˙ V
169 eqidd φ x Fin ¬ z x x z D y D if y x X y 0 ˙ = y D if y x X y 0 ˙
170 eqid R = R
171 1 7 10 6 170 2 127 133 mplvsca φ x Fin ¬ z x x z D X z · ˙ y D if y = z 1 ˙ 0 ˙ = D × X z R f y D if y = z 1 ˙ 0 ˙
172 127 adantr φ x Fin ¬ z x x z D y D X z Base R
173 10 4 ringidcl R Ring 1 ˙ Base R
174 173 144 ifcld R Ring if y = z 1 ˙ 0 ˙ Base R
175 8 174 syl φ if y = z 1 ˙ 0 ˙ Base R
176 175 ad2antrr φ x Fin ¬ z x x z D y D if y = z 1 ˙ 0 ˙ Base R
177 fconstmpt D × X z = y D X z
178 177 a1i φ x Fin ¬ z x x z D D × X z = y D X z
179 eqidd φ x Fin ¬ z x x z D y D if y = z 1 ˙ 0 ˙ = y D if y = z 1 ˙ 0 ˙
180 161 172 176 178 179 offval2 φ x Fin ¬ z x x z D D × X z R f y D if y = z 1 ˙ 0 ˙ = y D X z R if y = z 1 ˙ 0 ˙
181 171 180 eqtrd φ x Fin ¬ z x x z D X z · ˙ y D if y = z 1 ˙ 0 ˙ = y D X z R if y = z 1 ˙ 0 ˙
182 161 147 168 169 181 offval2 φ x Fin ¬ z x x z D y D if y x X y 0 ˙ + R f X z · ˙ y D if y = z 1 ˙ 0 ˙ = y D if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙
183 132 82 syl φ x Fin ¬ z x x z D R Grp
184 10 142 3 grplid R Grp X z Base R 0 ˙ + R X z = X z
185 183 127 184 syl2anc φ x Fin ¬ z x x z D 0 ˙ + R X z = X z
186 185 ad2antrr φ x Fin ¬ z x x z D y D y z 0 ˙ + R X z = X z
187 simpr φ x Fin ¬ z x x z D y D y z y z
188 velsn y z y = z
189 187 188 sylib φ x Fin ¬ z x x z D y D y z y = z
190 189 fveq2d φ x Fin ¬ z x x z D y D y z X y = X z
191 186 190 eqtr4d φ x Fin ¬ z x x z D y D y z 0 ˙ + R X z = X y
192 120 ad2antrr φ x Fin ¬ z x x z D y D y z ¬ z x
193 189 192 eqneltrd φ x Fin ¬ z x x z D y D y z ¬ y x
194 193 iffalsed φ x Fin ¬ z x x z D y D y z if y x X y 0 ˙ = 0 ˙
195 189 iftrued φ x Fin ¬ z x x z D y D y z if y = z 1 ˙ 0 ˙ = 1 ˙
196 195 oveq2d φ x Fin ¬ z x x z D y D y z X z R if y = z 1 ˙ 0 ˙ = X z R 1 ˙
197 10 170 4 ringridm R Ring X z Base R X z R 1 ˙ = X z
198 132 127 197 syl2anc φ x Fin ¬ z x x z D X z R 1 ˙ = X z
199 198 ad2antrr φ x Fin ¬ z x x z D y D y z X z R 1 ˙ = X z
200 196 199 eqtrd φ x Fin ¬ z x x z D y D y z X z R if y = z 1 ˙ 0 ˙ = X z
201 194 200 oveq12d φ x Fin ¬ z x x z D y D y z if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = 0 ˙ + R X z
202 elun2 y z y x z
203 202 adantl φ x Fin ¬ z x x z D y D y z y x z
204 203 iftrued φ x Fin ¬ z x x z D y D y z if y x z X y 0 ˙ = X y
205 191 201 204 3eqtr4d φ x Fin ¬ z x x z D y D y z if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = if y x z X y 0 ˙
206 83 ad2antrr φ x Fin ¬ z x x z D y D R Grp
207 10 142 3 grprid R Grp if y x X y 0 ˙ Base R if y x X y 0 ˙ + R 0 ˙ = if y x X y 0 ˙
208 206 147 207 syl2anc φ x Fin ¬ z x x z D y D if y x X y 0 ˙ + R 0 ˙ = if y x X y 0 ˙
209 208 adantr φ x Fin ¬ z x x z D y D ¬ y z if y x X y 0 ˙ + R 0 ˙ = if y x X y 0 ˙
210 simpr φ x Fin ¬ z x x z D y D ¬ y z ¬ y z
211 210 188 sylnib φ x Fin ¬ z x x z D y D ¬ y z ¬ y = z
212 211 iffalsed φ x Fin ¬ z x x z D y D ¬ y z if y = z 1 ˙ 0 ˙ = 0 ˙
213 212 oveq2d φ x Fin ¬ z x x z D y D ¬ y z X z R if y = z 1 ˙ 0 ˙ = X z R 0 ˙
214 10 170 3 ringrz R Ring X z Base R X z R 0 ˙ = 0 ˙
215 132 127 214 syl2anc φ x Fin ¬ z x x z D X z R 0 ˙ = 0 ˙
216 215 ad2antrr φ x Fin ¬ z x x z D y D ¬ y z X z R 0 ˙ = 0 ˙
217 213 216 eqtrd φ x Fin ¬ z x x z D y D ¬ y z X z R if y = z 1 ˙ 0 ˙ = 0 ˙
218 217 oveq2d φ x Fin ¬ z x x z D y D ¬ y z if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = if y x X y 0 ˙ + R 0 ˙
219 elun y x z y x y z
220 orcom y x y z y z y x
221 219 220 bitri y x z y z y x
222 biorf ¬ y z y x y z y x
223 221 222 bitr4id ¬ y z y x z y x
224 223 adantl φ x Fin ¬ z x x z D y D ¬ y z y x z y x
225 224 ifbid φ x Fin ¬ z x x z D y D ¬ y z if y x z X y 0 ˙ = if y x X y 0 ˙
226 209 218 225 3eqtr4d φ x Fin ¬ z x x z D y D ¬ y z if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = if y x z X y 0 ˙
227 205 226 pm2.61dan φ x Fin ¬ z x x z D y D if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = if y x z X y 0 ˙
228 227 mpteq2dva φ x Fin ¬ z x x z D y D if y x X y 0 ˙ + R X z R if y = z 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
229 167 182 228 3eqtrrd φ x Fin ¬ z x x z D y D if y x z X y 0 ˙ = y D if y x X y 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙
230 141 229 eqeq12d φ x Fin ¬ z x x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙ P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙ = y D if y x X y 0 ˙ + P X z · ˙ y D if y = z 1 ˙ 0 ˙
231 92 230 imbitrrid φ x Fin ¬ z x x z D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
232 231 expr φ x Fin ¬ z x x z D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
233 232 a2d φ x Fin ¬ z x x z D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
234 91 233 syl5 φ x Fin ¬ z x x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
235 234 expcom x Fin ¬ z x φ x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
236 235 a2d x Fin ¬ z x φ x D P k x X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x X y 0 ˙ φ x z D P k x z X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y x z X y 0 ˙
237 54 63 72 81 87 236 findcard2s X supp 0 ˙ Fin φ X supp 0 ˙ D P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
238 38 237 mpcom φ X supp 0 ˙ D P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
239 32 238 mpd φ P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = y D if y supp 0 ˙ X X y 0 ˙
240 30 239 eqtr4d φ X = P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙
241 32 resmptd φ k D X k · ˙ y D if y = k 1 ˙ 0 ˙ supp 0 ˙ X = k supp 0 ˙ X X k · ˙ y D if y = k 1 ˙ 0 ˙
242 241 oveq2d φ P k D X k · ˙ y D if y = k 1 ˙ 0 ˙ supp 0 ˙ X = P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙
243 115 fmpttd φ k D X k · ˙ y D if y = k 1 ˙ 0 ˙ : D B
244 11 16 19 21 suppssr φ k D supp 0 ˙ X X k = 0 ˙
245 244 oveq1d φ k D supp 0 ˙ X X k · ˙ y D if y = k 1 ˙ 0 ˙ = 0 ˙ · ˙ y D if y = k 1 ˙ 0 ˙
246 eldifi k D supp 0 ˙ X k D
247 107 fveq2d φ k D 0 R = 0 Scalar P
248 3 247 eqtrid φ k D 0 ˙ = 0 Scalar P
249 248 oveq1d φ k D 0 ˙ · ˙ y D if y = k 1 ˙ 0 ˙ = 0 Scalar P · ˙ y D if y = k 1 ˙ 0 ˙
250 eqid 0 Scalar P = 0 Scalar P
251 6 112 7 250 44 lmod0vs P LMod y D if y = k 1 ˙ 0 ˙ B 0 Scalar P · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
252 104 111 251 syl2anc φ k D 0 Scalar P · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
253 249 252 eqtrd φ k D 0 ˙ · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
254 246 253 sylan2 φ k D supp 0 ˙ X 0 ˙ · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
255 245 254 eqtrd φ k D supp 0 ˙ X X k · ˙ y D if y = k 1 ˙ 0 ˙ = 0 P
256 255 19 suppss2 φ k D X k · ˙ y D if y = k 1 ˙ 0 ˙ supp 0 P X supp 0 ˙
257 18 mptex k D X k · ˙ y D if y = k 1 ˙ 0 ˙ V
258 funmpt Fun k D X k · ˙ y D if y = k 1 ˙ 0 ˙
259 fvex 0 P V
260 257 258 259 3pm3.2i k D X k · ˙ y D if y = k 1 ˙ 0 ˙ V Fun k D X k · ˙ y D if y = k 1 ˙ 0 ˙ 0 P V
261 260 a1i φ k D X k · ˙ y D if y = k 1 ˙ 0 ˙ V Fun k D X k · ˙ y D if y = k 1 ˙ 0 ˙ 0 P V
262 suppssfifsupp k D X k · ˙ y D if y = k 1 ˙ 0 ˙ V Fun k D X k · ˙ y D if y = k 1 ˙ 0 ˙ 0 P V X supp 0 ˙ Fin k D X k · ˙ y D if y = k 1 ˙ 0 ˙ supp 0 P X supp 0 ˙ finSupp 0 P k D X k · ˙ y D if y = k 1 ˙ 0 ˙
263 261 38 256 262 syl12anc φ finSupp 0 P k D X k · ˙ y D if y = k 1 ˙ 0 ˙
264 6 44 96 19 243 256 263 gsumres φ P k D X k · ˙ y D if y = k 1 ˙ 0 ˙ supp 0 ˙ X = P k D X k · ˙ y D if y = k 1 ˙ 0 ˙
265 242 264 eqtr3d φ P k X supp 0 ˙ X k · ˙ y D if y = k 1 ˙ 0 ˙ = P k D X k · ˙ y D if y = k 1 ˙ 0 ˙
266 240 265 eqtrd φ X = P k D X k · ˙ y D if y = k 1 ˙ 0 ˙