Metamath Proof Explorer

Theorem chpdmat

Description: The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019) (Proof shortened by AV, 21-Nov-2019)

Ref Expression
Hypotheses chpdmat.c 
|- C = ( N CharPlyMat R )
chpdmat.p 
|- P = ( Poly1 ` R )
chpdmat.a 
|- A = ( N Mat R )
chpdmat.s 
|- S = ( algSc ` P )
chpdmat.b 
|- B = ( Base ` A )
chpdmat.x 
|- X = ( var1 ` R )
chpdmat.0 
|- .0. = ( 0g ` R )
chpdmat.g 
|- G = ( mulGrp ` P )
chpdmat.m 
|- .- = ( -g ` P )
Assertion chpdmat 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( C ` M ) = ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpdmat.c 
 |-  C = ( N CharPlyMat R )
2 chpdmat.p 
 |-  P = ( Poly1 ` R )
3 chpdmat.a 
 |-  A = ( N Mat R )
4 chpdmat.s 
 |-  S = ( algSc ` P )
5 chpdmat.b 
 |-  B = ( Base ` A )
6 chpdmat.x 
 |-  X = ( var1 ` R )
7 chpdmat.0 
 |-  .0. = ( 0g ` R )
8 chpdmat.g 
 |-  G = ( mulGrp ` P )
9 chpdmat.m 
 |-  .- = ( -g ` P )
10 eqid 
 |-  ( N Mat P ) = ( N Mat P )
11 eqid 
 |-  ( N maDet P ) = ( N maDet P )
12 eqid 
 |-  ( -g ` ( N Mat P ) ) = ( -g ` ( N Mat P ) )
13 eqid 
 |-  ( .s ` ( N Mat P ) ) = ( .s ` ( N Mat P ) )
14 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
15 eqid 
 |-  ( 1r ` ( N Mat P ) ) = ( 1r ` ( N Mat P ) )
16 1 3 5 2 10 11 12 6 13 14 15 chpmatval 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) )
17 16 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) )
18 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
19 18 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. CRing )
20 simp1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> N e. Fin )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 21 3anim2i 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring /\ M e. B ) )
23 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) )
24 22 23 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) )
25 19 20 24 3jca 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( P e. CRing /\ N e. Fin /\ ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) ) )
26 25 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( P e. CRing /\ N e. Fin /\ ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) ) )
27 22 anim1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) -> ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) )
28 27 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) )
29 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem2 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) )
30 28 29 sylanl1 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) )
31 30 exp31 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( i =/= j -> ( ( i M j ) = .0. -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) ) )
32 31 a2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( ( i =/= j -> ( i M j ) = .0. ) -> ( i =/= j -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) ) )
33 32 ralimdva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. N ) -> ( A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> A. j e. N ( i =/= j -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) ) )
34 33 ralimdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) ) )
35 34 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) )
36 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
37 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
38 11 10 36 8 37 mdetdiag 
 |-  ( ( P e. CRing /\ N e. Fin /\ ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) j ) = ( 0g ` P ) ) -> ( ( N maDet P ) ` ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) = ( G gsum ( k e. N |-> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) ) ) ) )
39 26 35 38 sylc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( ( N maDet P ) ` ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) = ( G gsum ( k e. N |-> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) ) ) )
40 1 2 3 4 5 6 7 8 9 10 15 13 12 14 chpdmatlem3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. N ) -> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) = ( X .- ( S ` ( k M k ) ) ) )
41 22 40 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ k e. N ) -> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) = ( X .- ( S ` ( k M k ) ) ) )
42 41 adantlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ k e. N ) -> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) = ( X .- ( S ` ( k M k ) ) ) )
43 42 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( k e. N |-> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) ) = ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) )
44 43 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( G gsum ( k e. N |-> ( k ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) k ) ) ) = ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) )
45 17 39 44 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( C ` M ) = ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) )