Metamath Proof Explorer


Theorem mp2pm2mplem4

Description: Lemma 4 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses mp2pm2mp.a A = N Mat R
mp2pm2mp.q Q = Poly 1 A
mp2pm2mp.l L = Base Q
mp2pm2mp.m · ˙ = P
mp2pm2mp.e E = mulGrp P
mp2pm2mp.y Y = var 1 R
mp2pm2mp.i I = p L i N , j N P k 0 i coe 1 p k j · ˙ k E Y
mp2pm2mplem2.p P = Poly 1 R
Assertion mp2pm2mplem4 N Fin R Ring O L K 0 I O decompPMat K = coe 1 O K

Proof

Step Hyp Ref Expression
1 mp2pm2mp.a A = N Mat R
2 mp2pm2mp.q Q = Poly 1 A
3 mp2pm2mp.l L = Base Q
4 mp2pm2mp.m · ˙ = P
5 mp2pm2mp.e E = mulGrp P
6 mp2pm2mp.y Y = var 1 R
7 mp2pm2mp.i I = p L i N , j N P k 0 i coe 1 p k j · ˙ k E Y
8 mp2pm2mplem2.p P = Poly 1 R
9 1 2 3 4 5 6 7 8 mp2pm2mplem3 N Fin R Ring O L K 0 I O decompPMat K = i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K
10 eqid Base P = Base P
11 eqid 0 P = 0 P
12 8 ply1ring R Ring P Ring
13 12 3ad2ant2 N Fin R Ring O L P Ring
14 ringcmn P Ring P CMnd
15 13 14 syl N Fin R Ring O L P CMnd
16 15 ad3antrrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A P CMnd
17 16 3ad2ant1 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N P CMnd
18 simpl2 N Fin R Ring O L K 0 R Ring
19 18 ad2antrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A R Ring
20 19 3ad2ant1 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N R Ring
21 20 adantr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 R Ring
22 eqid Base R = Base R
23 eqid Base A = Base A
24 simpl2 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i N
25 simpl3 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 j N
26 simpl3 N Fin R Ring O L K 0 O L
27 26 ad2antrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A O L
28 27 3ad2ant1 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N O L
29 eqid coe 1 O = coe 1 O
30 29 3 2 23 coe1fvalcl O L k 0 coe 1 O k Base A
31 28 30 sylan N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 coe 1 O k Base A
32 1 22 23 24 25 31 matecld N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i coe 1 O k j Base R
33 simpr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 k 0
34 eqid mulGrp P = mulGrp P
35 22 8 6 4 34 5 10 ply1tmcl R Ring i coe 1 O k j Base R k 0 i coe 1 O k j · ˙ k E Y Base P
36 21 32 33 35 syl3anc N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i coe 1 O k j · ˙ k E Y Base P
37 36 ralrimiva N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i coe 1 O k j · ˙ k E Y Base P
38 simp1lr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N s 0
39 oveq coe 1 O x = 0 A i coe 1 O x j = i 0 A j
40 39 oveq1d coe 1 O x = 0 A i coe 1 O x j · ˙ x E Y = i 0 A j · ˙ x E Y
41 3simpa N Fin R Ring O L N Fin R Ring
42 41 ad3antrrr N Fin R Ring O L K 0 s 0 i N j N N Fin R Ring
43 eqid 0 R = 0 R
44 1 43 mat0op N Fin R Ring 0 A = a N , b N 0 R
45 42 44 syl N Fin R Ring O L K 0 s 0 i N j N 0 A = a N , b N 0 R
46 eqidd N Fin R Ring O L K 0 s 0 i N j N a = i b = j 0 R = 0 R
47 simprl N Fin R Ring O L K 0 s 0 i N j N i N
48 simprr N Fin R Ring O L K 0 s 0 i N j N j N
49 fvexd N Fin R Ring O L K 0 s 0 i N j N 0 R V
50 45 46 47 48 49 ovmpod N Fin R Ring O L K 0 s 0 i N j N i 0 A j = 0 R
51 50 adantr N Fin R Ring O L K 0 s 0 i N j N x 0 i 0 A j = 0 R
52 51 oveq1d N Fin R Ring O L K 0 s 0 i N j N x 0 i 0 A j · ˙ x E Y = 0 R · ˙ x E Y
53 18 ad3antrrr N Fin R Ring O L K 0 s 0 i N j N x 0 R Ring
54 8 ply1sca R Ring R = Scalar P
55 53 54 syl N Fin R Ring O L K 0 s 0 i N j N x 0 R = Scalar P
56 55 fveq2d N Fin R Ring O L K 0 s 0 i N j N x 0 0 R = 0 Scalar P
57 56 oveq1d N Fin R Ring O L K 0 s 0 i N j N x 0 0 R · ˙ x E Y = 0 Scalar P · ˙ x E Y
58 8 ply1lmod R Ring P LMod
59 58 3ad2ant2 N Fin R Ring O L P LMod
60 59 ad4antr N Fin R Ring O L K 0 s 0 i N j N x 0 P LMod
61 simpr N Fin R Ring O L K 0 s 0 i N j N x 0 x 0
62 8 6 34 5 10 ply1moncl R Ring x 0 x E Y Base P
63 53 61 62 syl2anc N Fin R Ring O L K 0 s 0 i N j N x 0 x E Y Base P
64 eqid Scalar P = Scalar P
65 eqid 0 Scalar P = 0 Scalar P
66 10 64 4 65 11 lmod0vs P LMod x E Y Base P 0 Scalar P · ˙ x E Y = 0 P
67 60 63 66 syl2anc N Fin R Ring O L K 0 s 0 i N j N x 0 0 Scalar P · ˙ x E Y = 0 P
68 52 57 67 3eqtrd N Fin R Ring O L K 0 s 0 i N j N x 0 i 0 A j · ˙ x E Y = 0 P
69 68 adantr N Fin R Ring O L K 0 s 0 i N j N x 0 s < x i 0 A j · ˙ x E Y = 0 P
70 40 69 sylan9eqr N Fin R Ring O L K 0 s 0 i N j N x 0 s < x coe 1 O x = 0 A i coe 1 O x j · ˙ x E Y = 0 P
71 70 exp31 N Fin R Ring O L K 0 s 0 i N j N x 0 s < x coe 1 O x = 0 A i coe 1 O x j · ˙ x E Y = 0 P
72 71 a2d N Fin R Ring O L K 0 s 0 i N j N x 0 s < x coe 1 O x = 0 A s < x i coe 1 O x j · ˙ x E Y = 0 P
73 72 ralimdva N Fin R Ring O L K 0 s 0 i N j N x 0 s < x coe 1 O x = 0 A x 0 s < x i coe 1 O x j · ˙ x E Y = 0 P
74 73 impancom N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N x 0 s < x i coe 1 O x j · ˙ x E Y = 0 P
75 74 3impib N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N x 0 s < x i coe 1 O x j · ˙ x E Y = 0 P
76 breq2 k = x s < k s < x
77 fveq2 k = x coe 1 O k = coe 1 O x
78 77 oveqd k = x i coe 1 O k j = i coe 1 O x j
79 oveq1 k = x k E Y = x E Y
80 78 79 oveq12d k = x i coe 1 O k j · ˙ k E Y = i coe 1 O x j · ˙ x E Y
81 80 eqeq1d k = x i coe 1 O k j · ˙ k E Y = 0 P i coe 1 O x j · ˙ x E Y = 0 P
82 76 81 imbi12d k = x s < k i coe 1 O k j · ˙ k E Y = 0 P s < x i coe 1 O x j · ˙ x E Y = 0 P
83 82 cbvralvw k 0 s < k i coe 1 O k j · ˙ k E Y = 0 P x 0 s < x i coe 1 O x j · ˙ x E Y = 0 P
84 75 83 sylibr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 s < k i coe 1 O k j · ˙ k E Y = 0 P
85 10 11 17 37 38 84 gsummptnn0fz N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N P k 0 i coe 1 O k j · ˙ k E Y = P k = 0 s i coe 1 O k j · ˙ k E Y
86 85 fveq2d N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y = coe 1 P k = 0 s i coe 1 O k j · ˙ k E Y
87 86 fveq1d N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K = coe 1 P k = 0 s i coe 1 O k j · ˙ k E Y K
88 simpllr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A K 0
89 88 3ad2ant1 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N K 0
90 36 expcom k 0 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N i coe 1 O k j · ˙ k E Y Base P
91 elfznn0 k 0 s k 0
92 90 91 syl11 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 s i coe 1 O k j · ˙ k E Y Base P
93 92 ralrimiv N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 s i coe 1 O k j · ˙ k E Y Base P
94 fzfid N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N 0 s Fin
95 8 10 20 89 93 94 coe1fzgsumd N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N coe 1 P k = 0 s i coe 1 O k j · ˙ k E Y K = R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K
96 87 95 eqtrd N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K = R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K
97 96 mpoeq3dva N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K = i N , j N R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K
98 18 3ad2ant1 N Fin R Ring O L K 0 i N j N R Ring
99 98 adantr N Fin R Ring O L K 0 i N j N k 0 s R Ring
100 simpl2 N Fin R Ring O L K 0 i N j N k 0 s i N
101 simpl3 N Fin R Ring O L K 0 i N j N k 0 s j N
102 26 3ad2ant1 N Fin R Ring O L K 0 i N j N O L
103 102 91 30 syl2an N Fin R Ring O L K 0 i N j N k 0 s coe 1 O k Base A
104 1 22 23 100 101 103 matecld N Fin R Ring O L K 0 i N j N k 0 s i coe 1 O k j Base R
105 91 adantl N Fin R Ring O L K 0 i N j N k 0 s k 0
106 43 22 8 6 4 34 5 coe1tm R Ring i coe 1 O k j Base R k 0 coe 1 i coe 1 O k j · ˙ k E Y = l 0 if l = k i coe 1 O k j 0 R
107 99 104 105 106 syl3anc N Fin R Ring O L K 0 i N j N k 0 s coe 1 i coe 1 O k j · ˙ k E Y = l 0 if l = k i coe 1 O k j 0 R
108 eqeq1 l = K l = k K = k
109 108 ifbid l = K if l = k i coe 1 O k j 0 R = if K = k i coe 1 O k j 0 R
110 109 adantl N Fin R Ring O L K 0 i N j N k 0 s l = K if l = k i coe 1 O k j 0 R = if K = k i coe 1 O k j 0 R
111 simpl1r N Fin R Ring O L K 0 i N j N k 0 s K 0
112 ovex i coe 1 O k j V
113 fvex 0 R V
114 112 113 ifex if K = k i coe 1 O k j 0 R V
115 114 a1i N Fin R Ring O L K 0 i N j N k 0 s if K = k i coe 1 O k j 0 R V
116 107 110 111 115 fvmptd N Fin R Ring O L K 0 i N j N k 0 s coe 1 i coe 1 O k j · ˙ k E Y K = if K = k i coe 1 O k j 0 R
117 116 mpteq2dva N Fin R Ring O L K 0 i N j N k 0 s coe 1 i coe 1 O k j · ˙ k E Y K = k 0 s if K = k i coe 1 O k j 0 R
118 117 oveq2d N Fin R Ring O L K 0 i N j N R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K = R k = 0 s if K = k i coe 1 O k j 0 R
119 118 mpoeq3dva N Fin R Ring O L K 0 i N , j N R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K = i N , j N R k = 0 s if K = k i coe 1 O k j 0 R
120 119 ad2antrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s coe 1 i coe 1 O k j · ˙ k E Y K = i N , j N R k = 0 s if K = k i coe 1 O k j 0 R
121 breq2 x = K s < x s < K
122 fveqeq2 x = K coe 1 O x = 0 A coe 1 O K = 0 A
123 121 122 imbi12d x = K s < x coe 1 O x = 0 A s < K coe 1 O K = 0 A
124 123 rspcva K 0 x 0 s < x coe 1 O x = 0 A s < K coe 1 O K = 0 A
125 1 43 mat0op N Fin R Ring 0 A = i N , j N 0 R
126 125 eqcomd N Fin R Ring i N , j N 0 R = 0 A
127 126 3adant3 N Fin R Ring O L i N , j N 0 R = 0 A
128 127 ad3antlr K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N , j N 0 R = 0 A
129 elfz2nn0 k 0 s k 0 s 0 k s
130 nn0re k 0 k
131 130 ad2antrr k 0 s 0 K 0 k
132 nn0re s 0 s
133 132 ad2antlr k 0 s 0 K 0 s
134 nn0re K 0 K
135 134 adantl k 0 s 0 K 0 K
136 lelttr k s K k s s < K k < K
137 131 133 135 136 syl3anc k 0 s 0 K 0 k s s < K k < K
138 animorr k 0 s 0 K 0 k < K K < k k < K
139 df-ne K k ¬ K = k
140 130 adantr k 0 s 0 k
141 lttri2 K k K k K < k k < K
142 134 140 141 syl2anr k 0 s 0 K 0 K k K < k k < K
143 142 adantr k 0 s 0 K 0 k < K K k K < k k < K
144 139 143 syl5bbr k 0 s 0 K 0 k < K ¬ K = k K < k k < K
145 138 144 mpbird k 0 s 0 K 0 k < K ¬ K = k
146 145 ex k 0 s 0 K 0 k < K ¬ K = k
147 137 146 syld k 0 s 0 K 0 k s s < K ¬ K = k
148 147 exp4b k 0 s 0 K 0 k s s < K ¬ K = k
149 148 com24 k 0 s 0 s < K k s K 0 ¬ K = k
150 149 expimpd k 0 s 0 s < K k s K 0 ¬ K = k
151 150 com23 k 0 k s s 0 s < K K 0 ¬ K = k
152 151 imp k 0 k s s 0 s < K K 0 ¬ K = k
153 152 3adant2 k 0 s 0 k s s 0 s < K K 0 ¬ K = k
154 129 153 sylbi k 0 s s 0 s < K K 0 ¬ K = k
155 154 com13 K 0 s 0 s < K k 0 s ¬ K = k
156 155 adantr K 0 N Fin R Ring O L s 0 s < K k 0 s ¬ K = k
157 156 imp K 0 N Fin R Ring O L s 0 s < K k 0 s ¬ K = k
158 157 adantr K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A k 0 s ¬ K = k
159 158 3ad2ant1 K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N k 0 s ¬ K = k
160 159 imp K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N k 0 s ¬ K = k
161 160 iffalsed K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N k 0 s if K = k i coe 1 O k j 0 R = 0 R
162 161 mpteq2dva K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N k 0 s if K = k i coe 1 O k j 0 R = k 0 s 0 R
163 162 oveq2d K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N R k = 0 s if K = k i coe 1 O k j 0 R = R k = 0 s 0 R
164 ringmnd R Ring R Mnd
165 164 3ad2ant2 N Fin R Ring O L R Mnd
166 ovex 0 s V
167 43 gsumz R Mnd 0 s V R k = 0 s 0 R = 0 R
168 165 166 167 sylancl N Fin R Ring O L R k = 0 s 0 R = 0 R
169 168 ad3antlr K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A R k = 0 s 0 R = 0 R
170 169 3ad2ant1 K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N R k = 0 s 0 R = 0 R
171 163 170 eqtrd K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N j N R k = 0 s if K = k i coe 1 O k j 0 R = 0 R
172 171 mpoeq3dva K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = i N , j N 0 R
173 simpr K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A coe 1 O K = 0 A
174 128 172 173 3eqtr4d K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
175 174 ex K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
176 175 expr K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
177 176 a2d K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
178 177 exp31 K 0 N Fin R Ring O L s 0 s < K coe 1 O K = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
179 178 com14 s < K coe 1 O K = 0 A N Fin R Ring O L s 0 K 0 s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
180 124 179 syl K 0 x 0 s < x coe 1 O x = 0 A N Fin R Ring O L s 0 K 0 s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
181 180 ex K 0 x 0 s < x coe 1 O x = 0 A N Fin R Ring O L s 0 K 0 s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
182 181 com25 K 0 K 0 N Fin R Ring O L s 0 x 0 s < x coe 1 O x = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
183 182 pm2.43i K 0 N Fin R Ring O L s 0 x 0 s < x coe 1 O x = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
184 183 impcom N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
185 184 imp31 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A s < K i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
186 185 com12 s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
187 165 ad3antrrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A R Mnd
188 187 adantl ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A R Mnd
189 188 3ad2ant1 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N R Mnd
190 ovexd ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N 0 s V
191 lenlt K s K s ¬ s < K
192 134 132 191 syl2an K 0 s 0 K s ¬ s < K
193 simpll K 0 s 0 K s K 0
194 simplr K 0 s 0 K s s 0
195 simpr K 0 s 0 K s K s
196 elfz2nn0 K 0 s K 0 s 0 K s
197 193 194 195 196 syl3anbrc K 0 s 0 K s K 0 s
198 197 ex K 0 s 0 K s K 0 s
199 192 198 sylbird K 0 s 0 ¬ s < K K 0 s
200 199 ad4ant23 N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A ¬ s < K K 0 s
201 200 impcom ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A K 0 s
202 201 3ad2ant1 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N K 0 s
203 eqcom K = k k = K
204 ifbi K = k k = K if K = k i coe 1 O k j 0 R = if k = K i coe 1 O k j 0 R
205 203 204 ax-mp if K = k i coe 1 O k j 0 R = if k = K i coe 1 O k j 0 R
206 205 mpteq2i k 0 s if K = k i coe 1 O k j 0 R = k 0 s if k = K i coe 1 O k j 0 R
207 simpl2 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i N
208 simpl3 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 j N
209 27 adantl ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A O L
210 209 3ad2ant1 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N O L
211 210 30 sylan ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 coe 1 O k Base A
212 1 22 23 207 208 211 matecld ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 i coe 1 O k j Base R
213 91 212 sylan2 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 s i coe 1 O k j Base R
214 213 ralrimiva ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N k 0 s i coe 1 O k j Base R
215 43 189 190 202 206 214 gsummpt1n0 ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N j N R k = 0 s if K = k i coe 1 O k j 0 R = K / k i coe 1 O k j
216 215 mpoeq3dva ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = i N , j N K / k i coe 1 O k j
217 csbov K / k i coe 1 O k j = i K / k coe 1 O k j
218 csbfv K / k coe 1 O k = coe 1 O K
219 218 a1i K 0 K / k coe 1 O k = coe 1 O K
220 219 oveqd K 0 i K / k coe 1 O k j = i coe 1 O K j
221 217 220 syl5eq K 0 K / k i coe 1 O k j = i coe 1 O K j
222 221 ad2antlr N Fin R Ring O L K 0 a N b N K / k i coe 1 O k j = i coe 1 O K j
223 222 mpoeq3dv N Fin R Ring O L K 0 a N b N i N , j N K / k i coe 1 O k j = i N , j N i coe 1 O K j
224 oveq12 i = a j = b i coe 1 O K j = a coe 1 O K b
225 224 adantl N Fin R Ring O L K 0 a N b N i = a j = b i coe 1 O K j = a coe 1 O K b
226 simprl N Fin R Ring O L K 0 a N b N a N
227 simprr N Fin R Ring O L K 0 a N b N b N
228 ovexd N Fin R Ring O L K 0 a N b N a coe 1 O K b V
229 223 225 226 227 228 ovmpod N Fin R Ring O L K 0 a N b N a i N , j N K / k i coe 1 O k j b = a coe 1 O K b
230 229 ralrimivva N Fin R Ring O L K 0 a N b N a i N , j N K / k i coe 1 O k j b = a coe 1 O K b
231 simpl1 N Fin R Ring O L K 0 N Fin
232 218 oveqi i K / k coe 1 O k j = i coe 1 O K j
233 217 232 eqtri K / k i coe 1 O k j = i coe 1 O K j
234 simp2 N Fin R Ring O L K 0 i N j N i N
235 simp3 N Fin R Ring O L K 0 i N j N j N
236 29 3 2 23 coe1fvalcl O L K 0 coe 1 O K Base A
237 236 3ad2antl3 N Fin R Ring O L K 0 coe 1 O K Base A
238 237 3ad2ant1 N Fin R Ring O L K 0 i N j N coe 1 O K Base A
239 1 22 23 234 235 238 matecld N Fin R Ring O L K 0 i N j N i coe 1 O K j Base R
240 233 239 eqeltrid N Fin R Ring O L K 0 i N j N K / k i coe 1 O k j Base R
241 1 22 23 231 18 240 matbas2d N Fin R Ring O L K 0 i N , j N K / k i coe 1 O k j Base A
242 1 23 eqmat i N , j N K / k i coe 1 O k j Base A coe 1 O K Base A i N , j N K / k i coe 1 O k j = coe 1 O K a N b N a i N , j N K / k i coe 1 O k j b = a coe 1 O K b
243 241 237 242 syl2anc N Fin R Ring O L K 0 i N , j N K / k i coe 1 O k j = coe 1 O K a N b N a i N , j N K / k i coe 1 O k j b = a coe 1 O K b
244 230 243 mpbird N Fin R Ring O L K 0 i N , j N K / k i coe 1 O k j = coe 1 O K
245 244 ad2antrr N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N K / k i coe 1 O k j = coe 1 O K
246 245 adantl ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N K / k i coe 1 O k j = coe 1 O K
247 216 246 eqtrd ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
248 247 ex ¬ s < K N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
249 186 248 pm2.61i N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N R k = 0 s if K = k i coe 1 O k j 0 R = coe 1 O K
250 97 120 249 3eqtrd N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K = coe 1 O K
251 eqid 0 A = 0 A
252 29 3 2 251 coe1sfi O L finSupp 0 A coe 1 O
253 26 252 syl N Fin R Ring O L K 0 finSupp 0 A coe 1 O
254 29 3 2 251 23 coe1fsupp O L coe 1 O x Base A 0 | finSupp 0 A x
255 elrabi coe 1 O x Base A 0 | finSupp 0 A x coe 1 O Base A 0
256 26 254 255 3syl N Fin R Ring O L K 0 coe 1 O Base A 0
257 fvex 0 A V
258 fsuppmapnn0ub coe 1 O Base A 0 0 A V finSupp 0 A coe 1 O s 0 x 0 s < x coe 1 O x = 0 A
259 256 257 258 sylancl N Fin R Ring O L K 0 finSupp 0 A coe 1 O s 0 x 0 s < x coe 1 O x = 0 A
260 253 259 mpd N Fin R Ring O L K 0 s 0 x 0 s < x coe 1 O x = 0 A
261 250 260 r19.29a N Fin R Ring O L K 0 i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K = coe 1 O K
262 9 261 eqtrd N Fin R Ring O L K 0 I O decompPMat K = coe 1 O K