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 )
15 14 3ad2ant2
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )
16 15 adantr
 |-  ( ( ( 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 ) )
18 17 3adant3
 |-  ( ( 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 ) )
21 20 3ad2ant2
 |-  ( ( 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 )
23 22 3adant3
 |-  ( ( 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 ) )
29 28 adantr
 |-  ( ( ( 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 ) )
31 30 adantr
 |-  ( ( ( 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 )
39 14 adantl
 |-  ( ( N e. Fin /\ R e. Ring ) -> P e. Ring )
40 20 adantl
 |-  ( ( 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 ) ) )
42 41 3adant3
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring /\ X e. ( Base ` P ) ) )
43 42 adantr
 |-  ( ( ( 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. ) )
49 48 adantl
 |-  ( ( ( ( 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 )
52 51 adantl
 |-  ( ( ( 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 ) ) ) )