Metamath Proof Explorer

Theorem chpmatfval

Description: Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses chpmatfval.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpmatfval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chpmatfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
chpmatfval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chpmatfval.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
chpmatfval.d ⊢ 𝐷 = ( 𝑁 maDet 𝑃 )
chpmatfval.s ⊢ − = ( -g ‘ 𝑌 )
chpmatfval.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chpmatfval.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
chpmatfval.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chpmatfval.i ⊢ 1 = ( 1r ‘ 𝑌 )
Assertion chpmatfval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐶 = ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmatfval.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpmatfval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 chpmatfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 chpmatfval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5 chpmatfval.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
6 chpmatfval.d ⊢ 𝐷 = ( 𝑁 maDet 𝑃 )
7 chpmatfval.s ⊢ − = ( -g ‘ 𝑌 )
8 chpmatfval.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
9 chpmatfval.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
10 chpmatfval.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
11 chpmatfval.i ⊢ 1 = ( 1r ‘ 𝑌 )
12 df-chpmat ⊢ CharPlyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) )
13 12 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → CharPlyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) ) )
14 oveq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
15 14 2 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = 𝐴 )
16 15 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ 𝐴 ) )
17 16 3 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
18 simpl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
19 simpr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
20 19 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
21 20 4 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Poly1 ‘ 𝑟 ) = 𝑃 )
22 18 21 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) = ( 𝑁 maDet 𝑃 ) )
23 22 6 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) = 𝐷 )
24 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
25 24 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
26 25 4 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Poly1 ‘ 𝑟 ) = 𝑃 )
27 18 26 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) = ( 𝑁 Mat 𝑃 ) )
28 27 5 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) = 𝑌 )
29 28 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = ( -g ‘ 𝑌 ) )
30 29 7 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = − )
31 28 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = ( ·𝑠 ‘ 𝑌 ) )
32 31 9 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = · )
33 fveq2 ⊢ ( 𝑟 = 𝑅 → ( var1 ‘ 𝑟 ) = ( var1 ‘ 𝑅 ) )
34 33 8 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( var1 ‘ 𝑟 ) = 𝑋 )
35 34 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( var1 ‘ 𝑟 ) = 𝑋 )
36 28 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = ( 1r ‘ 𝑌 ) )
37 36 11 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) = 1 )
38 32 35 37 oveq123d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) = ( 𝑋 · 1 ) )
39 oveq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 matToPolyMat 𝑟 ) = ( 𝑁 matToPolyMat 𝑅 ) )
40 39 10 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 matToPolyMat 𝑟 ) = 𝑇 )
41 40 fveq1d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) = ( 𝑇 ‘ 𝑚 ) )
42 30 38 41 oveq123d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) )
43 23 42 fveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) = ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) )
44 17 43 mpteq12dv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) )
45 44 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) )
46 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
47 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
48 47 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ V )
49 3 fvexi ⊢ 𝐵 ∈ V
50 mptexg ⊢ ( 𝐵 ∈ V → ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) ∈ V )
51 49 50 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) ∈ V )
52 13 45 46 48 51 ovmpod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 CharPlyMat 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) )
53 1 52 syl5eq ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐶 = ( 𝑚 ∈ 𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑚 ) ) ) ) )