Metamath Proof Explorer


Theorem mp2pm2mplem3

Description: Lemma 3 for mp2pm2mp . (Contributed by AV, 10-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 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

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 mp2pm2mplem1 N Fin R Ring O L I O = i N , j N P k 0 i coe 1 O k j · ˙ k E Y
10 9 oveq1d N Fin R Ring O L I O decompPMat K = i N , j N P k 0 i coe 1 O k j · ˙ k E Y decompPMat K
11 10 adantr N Fin R Ring O L K 0 I O decompPMat K = i N , j N P k 0 i coe 1 O k j · ˙ k E Y decompPMat K
12 eqid N Mat P = N Mat P
13 eqid Base N Mat P = Base N Mat P
14 1 2 3 4 5 6 7 8 12 13 mp2pm2mplem2 N Fin R Ring O L i N , j N P k 0 i coe 1 O k j · ˙ k E Y Base N Mat P
15 12 13 decpmatval i N , j N P k 0 i coe 1 O k j · ˙ k E Y Base N Mat P K 0 i N , j N P k 0 i coe 1 O k j · ˙ k E Y decompPMat K = a N , b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b K
16 14 15 sylan N Fin R Ring O L K 0 i N , j N P k 0 i coe 1 O k j · ˙ k E Y decompPMat K = a N , b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b K
17 eqidd N Fin R Ring O L K 0 a N b N i N , j N P k 0 i coe 1 O k j · ˙ k E Y = i N , j N P k 0 i coe 1 O k j · ˙ k E Y
18 oveq12 i = a j = b i coe 1 O k j = a coe 1 O k b
19 18 oveq1d i = a j = b i coe 1 O k j · ˙ k E Y = a coe 1 O k b · ˙ k E Y
20 19 mpteq2dv i = a j = b k 0 i coe 1 O k j · ˙ k E Y = k 0 a coe 1 O k b · ˙ k E Y
21 20 oveq2d i = a j = b P k 0 i coe 1 O k j · ˙ k E Y = P k 0 a coe 1 O k b · ˙ k E Y
22 21 adantl N Fin R Ring O L K 0 a N b N i = a j = b P k 0 i coe 1 O k j · ˙ k E Y = P k 0 a coe 1 O k b · ˙ k E Y
23 simp2 N Fin R Ring O L K 0 a N b N a N
24 simp3 N Fin R Ring O L K 0 a N b N b N
25 ovexd N Fin R Ring O L K 0 a N b N P k 0 a coe 1 O k b · ˙ k E Y V
26 17 22 23 24 25 ovmpod N Fin R Ring O L K 0 a N b N a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b = P k 0 a coe 1 O k b · ˙ k E Y
27 26 fveq2d N Fin R Ring O L K 0 a N b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b = coe 1 P k 0 a coe 1 O k b · ˙ k E Y
28 27 fveq1d N Fin R Ring O L K 0 a N b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b K = coe 1 P k 0 a coe 1 O k b · ˙ k E Y K
29 28 mpoeq3dva N Fin R Ring O L K 0 a N , b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b K = a N , b N coe 1 P k 0 a coe 1 O k b · ˙ k E Y K
30 oveq1 a = i a coe 1 O k b = i coe 1 O k b
31 30 oveq1d a = i a coe 1 O k b · ˙ k E Y = i coe 1 O k b · ˙ k E Y
32 31 mpteq2dv a = i k 0 a coe 1 O k b · ˙ k E Y = k 0 i coe 1 O k b · ˙ k E Y
33 32 oveq2d a = i P k 0 a coe 1 O k b · ˙ k E Y = P k 0 i coe 1 O k b · ˙ k E Y
34 33 fveq2d a = i coe 1 P k 0 a coe 1 O k b · ˙ k E Y = coe 1 P k 0 i coe 1 O k b · ˙ k E Y
35 34 fveq1d a = i coe 1 P k 0 a coe 1 O k b · ˙ k E Y K = coe 1 P k 0 i coe 1 O k b · ˙ k E Y K
36 simpl b = j k 0 b = j
37 36 oveq2d b = j k 0 i coe 1 O k b = i coe 1 O k j
38 37 oveq1d b = j k 0 i coe 1 O k b · ˙ k E Y = i coe 1 O k j · ˙ k E Y
39 38 mpteq2dva b = j k 0 i coe 1 O k b · ˙ k E Y = k 0 i coe 1 O k j · ˙ k E Y
40 39 oveq2d b = j P k 0 i coe 1 O k b · ˙ k E Y = P k 0 i coe 1 O k j · ˙ k E Y
41 40 fveq2d b = j coe 1 P k 0 i coe 1 O k b · ˙ k E Y = coe 1 P k 0 i coe 1 O k j · ˙ k E Y
42 41 fveq1d b = j coe 1 P k 0 i coe 1 O k b · ˙ k E Y K = coe 1 P k 0 i coe 1 O k j · ˙ k E Y K
43 35 42 cbvmpov a N , b N coe 1 P k 0 a coe 1 O k b · ˙ k E Y K = i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K
44 29 43 syl6eq N Fin R Ring O L K 0 a N , b N coe 1 a i N , j N P k 0 i coe 1 O k j · ˙ k E Y b K = i N , j N coe 1 P k 0 i coe 1 O k j · ˙ k E Y K
45 11 16 44 3eqtrd 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