# 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 𝐴 = ( 𝑁 Mat 𝑅 )
chmatcl.b 𝐵 = ( Base ‘ 𝐴 )
chmatcl.p 𝑃 = ( Poly1𝑅 )
chmatcl.y 𝑌 = ( 𝑁 Mat 𝑃 )
chmatcl.x 𝑋 = ( var1𝑅 )
chmatcl.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chmatcl.s = ( -g𝑌 )
chmatcl.m · = ( ·𝑠𝑌 )
chmatcl.1 1 = ( 1r𝑌 )
chmatcl.h 𝐻 = ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) )
chmatval.s = ( -g𝑃 )
chmatval.0 0 = ( 0g𝑃 )
Assertion chmatval ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝑋 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) , ( 0 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) ) )

### Proof

Step Hyp Ref Expression
1 chmatcl.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 chmatcl.b 𝐵 = ( Base ‘ 𝐴 )
3 chmatcl.p 𝑃 = ( Poly1𝑅 )
4 chmatcl.y 𝑌 = ( 𝑁 Mat 𝑃 )
5 chmatcl.x 𝑋 = ( var1𝑅 )
6 chmatcl.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
7 chmatcl.s = ( -g𝑌 )
8 chmatcl.m · = ( ·𝑠𝑌 )
9 chmatcl.1 1 = ( 1r𝑌 )
10 chmatcl.h 𝐻 = ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) )
11 chmatval.s = ( -g𝑃 )
12 chmatval.0 0 = ( 0g𝑃 )
13 10 oveqi ( 𝐼 𝐻 𝐽 ) = ( 𝐼 ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝐽 )
14 3 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 14 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑃 ∈ Ring )
16 15 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝑃 ∈ Ring )
17 14 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
18 17 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
19 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20 5 3 19 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21 20 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
22 3 4 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
23 22 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑌 ∈ Ring )
24 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
25 24 9 ringidcl ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
26 23 25 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 1 ∈ ( Base ‘ 𝑌 ) )
27 19 4 24 8 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
28 18 21 26 27 syl12anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
29 28 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
30 6 1 2 3 4 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) )
31 30 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) )
32 simpr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼𝑁𝐽𝑁 ) )
33 4 24 7 11 matsubgcell ( ( 𝑃 ∈ Ring ∧ ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) )
34 16 29 31 32 33 syl121anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) )
35 13 34 syl5eq ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) )
36 9 a1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 1 = ( 1r𝑌 ) )
37 36 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑋 · 1 ) = ( 𝑋 · ( 1r𝑌 ) ) )
38 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
39 14 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
40 20 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
41 38 39 40 3jca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
42 41 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
43 42 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
44 4 19 8 12 matsc ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 · ( 1r𝑌 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
45 43 44 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑋 · ( 1r𝑌 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
46 37 45 eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑋 · 1 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
47 eqeq12 ( ( 𝑖 = 𝐼𝑗 = 𝐽 ) → ( 𝑖 = 𝑗𝐼 = 𝐽 ) )
48 47 ifbid ( ( 𝑖 = 𝐼𝑗 = 𝐽 ) → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
49 48 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) ∧ ( 𝑖 = 𝐼𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
50 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝐼𝑁 )
51 simpr ( ( 𝐼𝑁𝐽𝑁 ) → 𝐽𝑁 )
52 51 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝐽𝑁 )
53 5 fvexi 𝑋 ∈ V
54 12 fvexi 0 ∈ V
55 53 54 ifex if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∈ V
56 55 a1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∈ V )
57 46 49 50 52 56 ovmpod ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
58 57 oveq1d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) = ( if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) )
59 ovif ( if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) = if ( 𝐼 = 𝐽 , ( 𝑋 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) , ( 0 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) )
60 58 59 syl6eq ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) = if ( 𝐼 = 𝐽 , ( 𝑋 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) , ( 0 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) ) )
61 35 60 eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝑋 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) , ( 0 ( 𝐼 ( 𝑇𝑀 ) 𝐽 ) ) ) )