Metamath Proof Explorer


Theorem decpmatmullem

Description: Lemma for decpmatmul . (Contributed by AV, 20-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmatmul.p P = Poly 1 R
decpmatmul.c C = N Mat P
decpmatmul.b B = Base C
Assertion decpmatmullem N Fin R Ring U B W B I N J N K 0 I U C W decompPMat K J = R t N R l = 0 K coe 1 I U t l R coe 1 t W J K l

Proof

Step Hyp Ref Expression
1 decpmatmul.p P = Poly 1 R
2 decpmatmul.c C = N Mat P
3 decpmatmul.b B = Base C
4 simpr N Fin R Ring R Ring
5 4 3ad2ant1 N Fin R Ring U B W B I N J N K 0 R Ring
6 1 2 pmatring N Fin R Ring C Ring
7 6 adantr N Fin R Ring U B W B C Ring
8 simpl U B W B U B
9 8 adantl N Fin R Ring U B W B U B
10 simpr U B W B W B
11 10 adantl N Fin R Ring U B W B W B
12 eqid C = C
13 3 12 ringcl C Ring U B W B U C W B
14 7 9 11 13 syl3anc N Fin R Ring U B W B U C W B
15 14 3adant3 N Fin R Ring U B W B I N J N K 0 U C W B
16 simp33 N Fin R Ring U B W B I N J N K 0 K 0
17 3simpa I N J N K 0 I N J N
18 17 3ad2ant3 N Fin R Ring U B W B I N J N K 0 I N J N
19 1 2 3 decpmate R Ring U C W B K 0 I N J N I U C W decompPMat K J = coe 1 I U C W J K
20 5 15 16 18 19 syl31anc N Fin R Ring U B W B I N J N K 0 I U C W decompPMat K J = coe 1 I U C W J K
21 1 ply1ring R Ring P Ring
22 eqid P maMul N N N = P maMul N N N
23 2 22 matmulr N Fin P Ring P maMul N N N = C
24 23 eqcomd N Fin P Ring C = P maMul N N N
25 21 24 sylan2 N Fin R Ring C = P maMul N N N
26 25 3ad2ant1 N Fin R Ring U B W B I N J N K 0 C = P maMul N N N
27 26 oveqd N Fin R Ring U B W B I N J N K 0 U C W = U P maMul N N N W
28 27 oveqd N Fin R Ring U B W B I N J N K 0 I U C W J = I U P maMul N N N W J
29 eqid Base P = Base P
30 eqid P = P
31 21 adantl N Fin R Ring P Ring
32 31 3ad2ant1 N Fin R Ring U B W B I N J N K 0 P Ring
33 simpl N Fin R Ring N Fin
34 33 3ad2ant1 N Fin R Ring U B W B I N J N K 0 N Fin
35 2 29 matbas2 N Fin P Ring Base P N × N = Base C
36 3 35 eqtr4id N Fin P Ring B = Base P N × N
37 21 36 sylan2 N Fin R Ring B = Base P N × N
38 37 eleq2d N Fin R Ring U B U Base P N × N
39 38 biimpcd U B N Fin R Ring U Base P N × N
40 39 adantr U B W B N Fin R Ring U Base P N × N
41 40 impcom N Fin R Ring U B W B U Base P N × N
42 41 3adant3 N Fin R Ring U B W B I N J N K 0 U Base P N × N
43 21 35 sylan2 N Fin R Ring Base P N × N = Base C
44 3 43 eqtr4id N Fin R Ring B = Base P N × N
45 44 eleq2d N Fin R Ring W B W Base P N × N
46 45 biimpcd W B N Fin R Ring W Base P N × N
47 46 adantl U B W B N Fin R Ring W Base P N × N
48 47 impcom N Fin R Ring U B W B W Base P N × N
49 48 3adant3 N Fin R Ring U B W B I N J N K 0 W Base P N × N
50 simp31 N Fin R Ring U B W B I N J N K 0 I N
51 simp32 N Fin R Ring U B W B I N J N K 0 J N
52 22 29 30 32 34 34 34 42 49 50 51 mamufv N Fin R Ring U B W B I N J N K 0 I U P maMul N N N W J = P t N I U t P t W J
53 28 52 eqtrd N Fin R Ring U B W B I N J N K 0 I U C W J = P t N I U t P t W J
54 53 fveq2d N Fin R Ring U B W B I N J N K 0 coe 1 I U C W J = coe 1 P t N I U t P t W J
55 54 fveq1d N Fin R Ring U B W B I N J N K 0 coe 1 I U C W J K = coe 1 P t N I U t P t W J K
56 32 adantr N Fin R Ring U B W B I N J N K 0 t N P Ring
57 50 adantr N Fin R Ring U B W B I N J N K 0 t N I N
58 simpr N Fin R Ring U B W B I N J N K 0 t N t N
59 simpl2l N Fin R Ring U B W B I N J N K 0 t N U B
60 2 29 3 57 58 59 matecld N Fin R Ring U B W B I N J N K 0 t N I U t Base P
61 51 adantr N Fin R Ring U B W B I N J N K 0 t N J N
62 simpl2r N Fin R Ring U B W B I N J N K 0 t N W B
63 2 29 3 58 61 62 matecld N Fin R Ring U B W B I N J N K 0 t N t W J Base P
64 29 30 ringcl P Ring I U t Base P t W J Base P I U t P t W J Base P
65 56 60 63 64 syl3anc N Fin R Ring U B W B I N J N K 0 t N I U t P t W J Base P
66 65 ralrimiva N Fin R Ring U B W B I N J N K 0 t N I U t P t W J Base P
67 1 29 5 16 66 34 coe1fzgsumd N Fin R Ring U B W B I N J N K 0 coe 1 P t N I U t P t W J K = R t N coe 1 I U t P t W J K
68 simpl1r N Fin R Ring U B W B I N J N K 0 t N R Ring
69 eqid R = R
70 1 30 69 29 coe1mul R Ring I U t Base P t W J Base P coe 1 I U t P t W J = k 0 R l = 0 k coe 1 I U t l R coe 1 t W J k l
71 68 60 63 70 syl3anc N Fin R Ring U B W B I N J N K 0 t N coe 1 I U t P t W J = k 0 R l = 0 k coe 1 I U t l R coe 1 t W J k l
72 oveq2 k = K 0 k = 0 K
73 fvoveq1 k = K coe 1 t W J k l = coe 1 t W J K l
74 73 oveq2d k = K coe 1 I U t l R coe 1 t W J k l = coe 1 I U t l R coe 1 t W J K l
75 72 74 mpteq12dv k = K l 0 k coe 1 I U t l R coe 1 t W J k l = l 0 K coe 1 I U t l R coe 1 t W J K l
76 75 oveq2d k = K R l = 0 k coe 1 I U t l R coe 1 t W J k l = R l = 0 K coe 1 I U t l R coe 1 t W J K l
77 76 adantl N Fin R Ring U B W B I N J N K 0 t N k = K R l = 0 k coe 1 I U t l R coe 1 t W J k l = R l = 0 K coe 1 I U t l R coe 1 t W J K l
78 16 adantr N Fin R Ring U B W B I N J N K 0 t N K 0
79 ovexd N Fin R Ring U B W B I N J N K 0 t N R l = 0 K coe 1 I U t l R coe 1 t W J K l V
80 71 77 78 79 fvmptd N Fin R Ring U B W B I N J N K 0 t N coe 1 I U t P t W J K = R l = 0 K coe 1 I U t l R coe 1 t W J K l
81 80 mpteq2dva N Fin R Ring U B W B I N J N K 0 t N coe 1 I U t P t W J K = t N R l = 0 K coe 1 I U t l R coe 1 t W J K l
82 81 oveq2d N Fin R Ring U B W B I N J N K 0 R t N coe 1 I U t P t W J K = R t N R l = 0 K coe 1 I U t l R coe 1 t W J K l
83 67 82 eqtrd N Fin R Ring U B W B I N J N K 0 coe 1 P t N I U t P t W J K = R t N R l = 0 K coe 1 I U t l R coe 1 t W J K l
84 20 55 83 3eqtrd N Fin R Ring U B W B I N J N K 0 I U C W decompPMat K J = R t N R l = 0 K coe 1 I U t l R coe 1 t W J K l