Metamath Proof Explorer

Theorem cpmadugsumfi

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)

Ref Expression
Hypotheses cpmadugsum.a 
|- A = ( N Mat R )
cpmadugsum.b 
|- B = ( Base ` A )
cpmadugsum.p 
|- P = ( Poly1 ` R )
cpmadugsum.y 
|- Y = ( N Mat P )
cpmadugsum.t 
|- T = ( N matToPolyMat R )
cpmadugsum.x 
|- X = ( var1 ` R )
cpmadugsum.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
cpmadugsum.m 
|- .x. = ( .s ` Y )
cpmadugsum.r 
|- .X. = ( .r ` Y )
cpmadugsum.1 
|- .1. = ( 1r ` Y )
cpmadugsum.g 
|- .+ = ( +g ` Y )
cpmadugsum.s 
|- .- = ( -g ` Y )
cpmadugsum.i 
|- I = ( ( X .x. .1. ) .- ( T ` M ) )
cpmadugsum.j 
|- J = ( N maAdju P )
Assertion cpmadugsumfi 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a 
 |-  A = ( N Mat R )
2 cpmadugsum.b 
 |-  B = ( Base ` A )
3 cpmadugsum.p 
 |-  P = ( Poly1 ` R )
4 cpmadugsum.y 
 |-  Y = ( N Mat P )
5 cpmadugsum.t 
 |-  T = ( N matToPolyMat R )
6 cpmadugsum.x 
 |-  X = ( var1 ` R )
7 cpmadugsum.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
8 cpmadugsum.m 
 |-  .x. = ( .s ` Y )
9 cpmadugsum.r 
 |-  .X. = ( .r ` Y )
10 cpmadugsum.1 
 |-  .1. = ( 1r ` Y )
11 cpmadugsum.g 
 |-  .+ = ( +g ` Y )
12 cpmadugsum.s 
 |-  .- = ( -g ` Y )
13 cpmadugsum.i 
 |-  I = ( ( X .x. .1. ) .- ( T ` M ) )
14 cpmadugsum.j 
 |-  J = ( N maAdju P )
15 oveq2 
 |-  ( ( J ` I ) = ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( I .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) )
16 13 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> I = ( ( X .x. .1. ) .- ( T ` M ) ) )
17 16 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( I .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) = ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) )
18 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
19 crngring 
 |-  ( R e. CRing -> R e. Ring )
20 19 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
21 20 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
22 21 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( N e. Fin /\ R e. Ring ) )
23 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
24 22 23 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> Y e. Ring )
25 3 4 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
26 19 25 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
27 19 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
28 eqid 
 |-  ( Base ` P ) = ( Base ` P )
29 6 3 28 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
30 27 29 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
31 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
32 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
33 31 32 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P = ( Scalar ` Y ) )
34 33 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
35 30 34 eleqtrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` ( Scalar ` Y ) ) )
36 19 23 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
37 18 10 ringidcl 
 |-  ( Y e. Ring -> .1. e. ( Base ` Y ) )
38 36 37 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> .1. e. ( Base ` Y ) )
39 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
40 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
41 18 39 8 40 lmodvscl 
 |-  ( ( Y e. LMod /\ X e. ( Base ` ( Scalar ` Y ) ) /\ .1. e. ( Base ` Y ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
42 26 35 38 41 syl3anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( X .x. .1. ) e. ( Base ` Y ) )
43 42 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )
44 43 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
45 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
46 19 45 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
47 46 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
48 ringcmn 
 |-  ( Y e. Ring -> Y e. CMnd )
49 36 48 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. CMnd )
50 49 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
51 50 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> Y e. CMnd )
52 fzfid 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0 ... s ) e. Fin )
53 21 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. ( 0 ... s ) ) -> ( N e. Fin /\ R e. Ring ) )
54 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
55 ffvelrn 
 |-  ( ( b : ( 0 ... s ) --> B /\ n e. ( 0 ... s ) ) -> ( b ` n ) e. B )
56 55 ex 
 |-  ( b : ( 0 ... s ) --> B -> ( n e. ( 0 ... s ) -> ( b ` n ) e. B ) )
57 54 56 syl 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> ( n e. ( 0 ... s ) -> ( b ` n ) e. B ) )
58 57 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( n e. ( 0 ... s ) -> ( b ` n ) e. B ) )
59 58 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. ( 0 ... s ) ) -> ( b ` n ) e. B )
60 elfznn0 
 |-  ( n e. ( 0 ... s ) -> n e. NN0 )
61 60 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. ( 0 ... s ) ) -> n e. NN0 )
62 1 2 5 3 4 18 8 7 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` n ) e. B /\ n e. NN0 ) ) -> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
63 53 59 61 62 syl12anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ n e. ( 0 ... s ) ) -> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
64 63 ralrimiva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> A. n e. ( 0 ... s ) ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
65 18 51 52 64 gsummptcl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) e. ( Base ` Y ) )
66 18 9 12 24 44 47 65 rngsubdir 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) = ( ( ( X .x. .1. ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) ) )
67 oveq1 
 |-  ( n = i -> ( n .^ X ) = ( i .^ X ) )
68 2fveq3 
 |-  ( n = i -> ( T ` ( b ` n ) ) = ( T ` ( b ` i ) ) )
69 67 68 oveq12d 
 |-  ( n = i -> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) = ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
70 69 cbvmptv 
 |-  ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
71 70 oveq2i 
 |-  ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) )
72 71 oveq2i 
 |-  ( ( X .x. .1. ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) = ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
73 71 oveq2i 
 |-  ( ( T ` M ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) = ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
74 72 73 oveq12i 
 |-  ( ( ( X .x. .1. ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) ) = ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
75 1 2 3 4 5 6 7 8 9 10 11 12 cpmadugsumlemF 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
76 75 anassrs 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
77 74 76 syl5eq 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
78 17 66 77 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( I .X. ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
79 15 78 sylan9eqr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( J ` I ) = ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
80 4 14 18 maduf 
 |-  ( P e. CRing -> J : ( Base ` Y ) --> ( Base ` Y ) )
81 31 80 syl 
 |-  ( R e. CRing -> J : ( Base ` Y ) --> ( Base ` Y ) )
82 81 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> J : ( Base ` Y ) --> ( Base ` Y ) )
83 1 2 3 4 6 5 12 8 10 13 chmatcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> I e. ( Base ` Y ) )
84 19 83 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> I e. ( Base ` Y ) )
85 82 84 ffvelrnd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( J ` I ) e. ( Base ` Y ) )
86 3 4 18 8 7 6 5 1 2 pmatcollpw3fi1 
 |-  ( ( N e. Fin /\ R e. CRing /\ ( J ` I ) e. ( Base ` Y ) ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( J ` I ) = ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) )
87 85 86 syld3an3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( J ` I ) = ( Y gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .x. ( T ` ( b ` n ) ) ) ) ) )
88 79 87 reximddv2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )