Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cpmadugsumfi Structured version   Unicode version

 Description: The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019.) (Proof shortened by AV, 29-Nov-2019.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,,   ,   ,   ,,   ,,   ,,,   ,,,   ,,   ,,   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,,)   (,)   (,)   (,)

Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cpmadugsum.p . . . . . . 7 Poly1
21ply1crng 18008 . . . . . 6
3 cpmadugsum.y . . . . . . 7 Mat
5 eqid 2467 . . . . . . 7
63, 4, 5maduf 18910 . . . . . 6
72, 6syl 16 . . . . 5
873ad2ant2 1018 . . . 4
9 crngrng 16996 . . . . 5
10 cpmadugsum.a . . . . . 6 Mat
11 cpmadugsum.b . . . . . 6
12 cpmadugsum.x . . . . . 6 var1
13 cpmadugsum.t . . . . . 6 matToPolyMat
14 cpmadugsum.s . . . . . 6
15 cpmadugsum.m . . . . . 6
16 cpmadugsum.1 . . . . . 6
17 cpmadugsum.i . . . . . 6
1810, 11, 1, 3, 12, 13, 14, 15, 16, 17chmatcl 19096 . . . . 5
199, 18syl3an2 1262 . . . 4
208, 19ffvelrnd 6020 . . 3
21 cpmadugsum.e . . . 4 .gmulGrp
221, 3, 5, 15, 21, 12, 13, 10, 11pmatcollpw3fi1 19056 . . 3 g
2320, 22syld3an3 1273 . 2 g
24 oveq2 6290 . . . . . 6 g g
2517a1i 11 . . . . . . . 8
2625oveq1d 6297 . . . . . . 7 g g
27 cpmadugsum.r . . . . . . . 8
289anim2i 569 . . . . . . . . . . 11
29283adant3 1016 . . . . . . . . . 10
3029ad2antrr 725 . . . . . . . . 9
311, 3pmatrng 18961 . . . . . . . . 9
3230, 31syl 16 . . . . . . . 8
331, 3pmatlmod 18962 . . . . . . . . . . . 12
349, 33sylan2 474 . . . . . . . . . . 11
359adantl 466 . . . . . . . . . . . . 13
36 eqid 2467 . . . . . . . . . . . . . 14
3712, 1, 36vr1cl 18029 . . . . . . . . . . . . 13
3835, 37syl 16 . . . . . . . . . . . 12
393matsca2 18689 . . . . . . . . . . . . . 14 Scalar
402, 39sylan2 474 . . . . . . . . . . . . 13 Scalar
4140fveq2d 5868 . . . . . . . . . . . 12 Scalar
4238, 41eleqtrd 2557 . . . . . . . . . . 11 Scalar
439, 31sylan2 474 . . . . . . . . . . . 12
445, 16rngidcl 17006 . . . . . . . . . . . 12
4543, 44syl 16 . . . . . . . . . . 11
46 eqid 2467 . . . . . . . . . . . 12 Scalar Scalar
47 eqid 2467 . . . . . . . . . . . 12 Scalar Scalar
485, 46, 15, 47lmodvscl 17312 . . . . . . . . . . 11 Scalar
4934, 42, 45, 48syl3anc 1228 . . . . . . . . . 10
50493adant3 1016 . . . . . . . . 9
5150ad2antrr 725 . . . . . . . 8
5213, 10, 11, 1, 3mat2pmatbas 18994 . . . . . . . . . 10
539, 52syl3an2 1262 . . . . . . . . 9
5453ad2antrr 725 . . . . . . . 8
55 rngcmn 17016 . . . . . . . . . . . 12 CMnd
5643, 55syl 16 . . . . . . . . . . 11 CMnd
57563adant3 1016 . . . . . . . . . 10 CMnd
5857ad2antrr 725 . . . . . . . . 9 CMnd
59 fzfid 12047 . . . . . . . . 9
6029ad3antrrr 729 . . . . . . . . . . 11
61 elmapi 7437 . . . . . . . . . . . . . 14
62 ffvelrn 6017 . . . . . . . . . . . . . . 15
6362ex 434 . . . . . . . . . . . . . 14
6461, 63syl 16 . . . . . . . . . . . . 13
6564adantl 466 . . . . . . . . . . . 12
6665imp 429 . . . . . . . . . . 11
67 elfznn0 11766 . . . . . . . . . . . 12
6867adantl 466 . . . . . . . . . . 11
6910, 11, 13, 1, 3, 5, 15, 21, 12mat2pmatscmxcl 19008 . . . . . . . . . . 11
7060, 66, 68, 69syl12anc 1226 . . . . . . . . . 10
7170ralrimiva 2878 . . . . . . . . 9
725, 58, 59, 71gsummptcl 16785 . . . . . . . 8 g
735, 27, 14, 32, 51, 54, 72rngsubdir 17032 . . . . . . 7 g g g
74 oveq1 6289 . . . . . . . . . . . . 13
75 fveq2 5864 . . . . . . . . . . . . . 14
7675fveq2d 5868 . . . . . . . . . . . . 13
7774, 76oveq12d 6300 . . . . . . . . . . . 12
7877cbvmptv 4538 . . . . . . . . . . 11
7978oveq2i 6293 . . . . . . . . . 10 g g
8079oveq2i 6293 . . . . . . . . 9 g g
8179oveq2i 6293 . . . . . . . . 9 g g
8280, 81oveq12i 6294 . . . . . . . 8 g g g g
83 cpmadugsum.g . . . . . . . . . 10
8410, 11, 1, 3, 13, 12, 21, 15, 27, 16, 83, 14cpmadugsumlemF 19144 . . . . . . . . 9 g g g
8584anassrs 648 . . . . . . . 8 g g g
8682, 85syl5eq 2520 . . . . . . 7 g g g
8726, 73, 863eqtrd 2512 . . . . . 6 g g
8824, 87sylan9eqr 2530 . . . . 5 g g
8988ex 434 . . . 4 g g
9089reximdva 2938 . . 3 g g
9190reximdva 2938 . 2 g g
9223, 91mpd 15 1 g