# Metamath Proof Explorer

## Theorem chmatval

Description: The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019) (Proof shortened by AV, 10-Dec-2019)

Ref Expression
Hypotheses chmatcl.a
`|- A = ( N Mat R )`
chmatcl.b
`|- B = ( Base ` A )`
chmatcl.p
`|- P = ( Poly1 ` R )`
chmatcl.y
`|- Y = ( N Mat P )`
chmatcl.x
`|- X = ( var1 ` R )`
chmatcl.t
`|- T = ( N matToPolyMat R )`
chmatcl.s
`|- .- = ( -g ` Y )`
chmatcl.m
`|- .x. = ( .s ` Y )`
chmatcl.1
`|- .1. = ( 1r ` Y )`
chmatcl.h
`|- H = ( ( X .x. .1. ) .- ( T ` M ) )`
chmatval.s
`|- .~ = ( -g ` P )`
chmatval.0
`|- .0. = ( 0g ` P )`
Assertion chmatval
`|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I H J ) = if ( I = J , ( X .~ ( I ( T ` M ) J ) ) , ( .0. .~ ( I ( T ` M ) J ) ) ) )`

### Proof

Step Hyp Ref Expression
1 chmatcl.a
` |-  A = ( N Mat R )`
2 chmatcl.b
` |-  B = ( Base ` A )`
3 chmatcl.p
` |-  P = ( Poly1 ` R )`
4 chmatcl.y
` |-  Y = ( N Mat P )`
5 chmatcl.x
` |-  X = ( var1 ` R )`
6 chmatcl.t
` |-  T = ( N matToPolyMat R )`
7 chmatcl.s
` |-  .- = ( -g ` Y )`
8 chmatcl.m
` |-  .x. = ( .s ` Y )`
9 chmatcl.1
` |-  .1. = ( 1r ` Y )`
10 chmatcl.h
` |-  H = ( ( X .x. .1. ) .- ( T ` M ) )`
11 chmatval.s
` |-  .~ = ( -g ` P )`
12 chmatval.0
` |-  .0. = ( 0g ` P )`
13 10 oveqi
` |-  ( I H J ) = ( I ( ( X .x. .1. ) .- ( T ` M ) ) J )`
14 3 ply1ring
` |-  ( R e. Ring -> P e. Ring )`
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )`
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> P e. Ring )`
17 14 anim2i
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) )`
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )`
19 eqid
` |-  ( Base ` P ) = ( Base ` P )`
20 5 3 19 vr1cl
` |-  ( R e. Ring -> X e. ( Base ` P ) )`
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> X e. ( Base ` P ) )`
22 3 4 pmatring
` |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )`
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Ring )`
24 eqid
` |-  ( Base ` Y ) = ( Base ` Y )`
25 24 9 ringidcl
` |-  ( Y e. Ring -> .1. e. ( Base ` Y ) )`
26 23 25 syl
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .1. e. ( Base ` Y ) )`
27 19 4 24 8 matvscl
` |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Y ) ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )`
28 18 21 26 27 syl12anc
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )`
30 6 1 2 3 4 mat2pmatbas
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( T ` M ) e. ( Base ` Y ) )`
32 simpr
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I e. N /\ J e. N ) )`
33 4 24 7 11 matsubgcell
` |-  ( ( P e. Ring /\ ( ( X .x. .1. ) e. ( Base ` Y ) /\ ( T ` M ) e. ( Base ` Y ) ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( X .x. .1. ) .- ( T ` M ) ) J ) = ( ( I ( X .x. .1. ) J ) .~ ( I ( T ` M ) J ) ) )`
34 16 29 31 32 33 syl121anc
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( X .x. .1. ) .- ( T ` M ) ) J ) = ( ( I ( X .x. .1. ) J ) .~ ( I ( T ` M ) J ) ) )`
35 13 34 syl5eq
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I H J ) = ( ( I ( X .x. .1. ) J ) .~ ( I ( T ` M ) J ) ) )`
36 9 a1i
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> .1. = ( 1r ` Y ) )`
37 36 oveq2d
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X .x. .1. ) = ( X .x. ( 1r ` Y ) ) )`
38 simpl
` |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )`
` |-  ( ( N e. Fin /\ R e. Ring ) -> P e. Ring )`
` |-  ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` P ) )`
41 38 39 40 3jca
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring /\ X e. ( Base ` P ) ) )`
` |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring /\ X e. ( Base ` P ) ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( N e. Fin /\ P e. Ring /\ X e. ( Base ` P ) ) )`
44 4 19 8 12 matsc
` |-  ( ( N e. Fin /\ P e. Ring /\ X e. ( Base ` P ) ) -> ( X .x. ( 1r ` Y ) ) = ( i e. N , j e. N |-> if ( i = j , X , .0. ) ) )`
45 43 44 syl
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X .x. ( 1r ` Y ) ) = ( i e. N , j e. N |-> if ( i = j , X , .0. ) ) )`
46 37 45 eqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X .x. .1. ) = ( i e. N , j e. N |-> if ( i = j , X , .0. ) ) )`
47 eqeq12
` |-  ( ( i = I /\ j = J ) -> ( i = j <-> I = J ) )`
48 47 ifbid
` |-  ( ( i = I /\ j = J ) -> if ( i = j , X , .0. ) = if ( I = J , X , .0. ) )`
` |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( i = j , X , .0. ) = if ( I = J , X , .0. ) )`
50 simprl
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> I e. N )`
51 simpr
` |-  ( ( I e. N /\ J e. N ) -> J e. N )`
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> J e. N )`
53 5 fvexi
` |-  X e. _V`
54 12 fvexi
` |-  .0. e. _V`
55 53 54 ifex
` |-  if ( I = J , X , .0. ) e. _V`
56 55 a1i
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> if ( I = J , X , .0. ) e. _V )`
57 46 49 50 52 56 ovmpod
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .x. .1. ) J ) = if ( I = J , X , .0. ) )`
58 57 oveq1d
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( I ( X .x. .1. ) J ) .~ ( I ( T ` M ) J ) ) = ( if ( I = J , X , .0. ) .~ ( I ( T ` M ) J ) ) )`
59 ovif
` |-  ( if ( I = J , X , .0. ) .~ ( I ( T ` M ) J ) ) = if ( I = J , ( X .~ ( I ( T ` M ) J ) ) , ( .0. .~ ( I ( T ` M ) J ) ) )`
60 58 59 syl6eq
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( I ( X .x. .1. ) J ) .~ ( I ( T ` M ) J ) ) = if ( I = J , ( X .~ ( I ( T ` M ) J ) ) , ( .0. .~ ( I ( T ` M ) J ) ) ) )`
61 35 60 eqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I H J ) = if ( I = J , ( X .~ ( I ( T ` M ) J ) ) , ( .0. .~ ( I ( T ` M ) J ) ) ) )`