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 eqtrdi 
 |-  ( ( ( 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 ) ) ) )