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 eqtrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) ) )
61 35 60 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) ) )