Metamath Proof Explorer

Theorem idpm2idmp

Description: The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pm2mpval.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pm2mpval.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
pm2mpval.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
pm2mpval.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
pm2mpval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpval.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
pm2mpval.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion idpm2idmp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 1r ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pm2mpval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pm2mpval.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pm2mpval.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5 pm2mpval.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 pm2mpval.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
7 pm2mpval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8 pm2mpval.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9 pm2mpval.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
11 eqid ⊢ ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐶 )
12 3 11 ringidcl ⊢ ( 𝐶 ∈ Ring → ( 1r ‘ 𝐶 ) ∈ 𝐵 )
13 10 12 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) ∈ 𝐵 )
14 1 2 3 4 5 6 7 8 9 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
15 13 14 mpd3an3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
16 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
17 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
18 1 2 11 7 16 17 decpmatid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) = if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) )
19 18 3expa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) = if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) )
20 19 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
21 20 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
22 21 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 1r ‘ 𝐶 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
23 ovif ⊢ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 0 , ( ( 1r ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) , ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
24 7 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
25 8 ply1sca ⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
26 24 25 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
27 26 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
28 27 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( 1r ‘ 𝐴 ) = ( 1r ‘ ( Scalar ‘ 𝑄 ) ) )
29 28 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1r ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
30 8 ply1lmod ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
31 24 30 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
32 eqid ⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
33 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
34 8 6 32 5 33 ply1moncl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
35 24 34 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
36 eqid ⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
37 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑄 ) ) = ( 1r ‘ ( Scalar ‘ 𝑄 ) )
38 33 36 4 37 lmodvs1 ⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑘 ↑ 𝑋 ) )
39 31 35 38 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1r ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑘 ↑ 𝑋 ) )
40 29 39 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1r ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑘 ↑ 𝑋 ) )
41 27 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( 0g ‘ 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
42 41 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
43 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
44 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
45 33 36 4 43 44 lmod0vs ⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
46 31 35 45 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
47 42 46 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
48 40 47 ifeq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 0 , ( ( 1r ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) , ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) )
49 23 48 eqtrid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) )
50 49 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) ) )
51 50 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) ) ) )
52 8 ply1ring ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
53 ringmnd ⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Mnd )
54 24 52 53 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Mnd )
55 nn0ex ⊢ ℕ0 ∈ V
56 55 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ℕ0 ∈ V )
57 0nn0 ⊢ 0 ∈ ℕ0
58 57 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 ∈ ℕ0 )
59 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) )
60 35 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑘 ∈ ℕ0 ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
61 44 54 56 58 59 60 gsummpt1n0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( 𝑘 ↑ 𝑋 ) , ( 0g ‘ 𝑄 ) ) ) ) = ⦋ 0 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) )
62 c0ex ⊢ 0 ∈ V
63 csbov1g ⊢ ( 0 ∈ V → ⦋ 0 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( ⦋ 0 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) )
64 62 63 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ⦋ 0 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( ⦋ 0 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) )
65 csbvarg ⊢ ( 0 ∈ V → ⦋ 0 / 𝑘 ⦌ 𝑘 = 0 )
66 62 65 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ⦋ 0 / 𝑘 ⦌ 𝑘 = 0 )
67 66 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ⦋ 0 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
68 8 6 32 5 ply1idvr1 ⊢ ( 𝐴 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑄 ) )
69 24 68 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑄 ) )
70 64 67 69 3eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ⦋ 0 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( 1r ‘ 𝑄 ) )
71 51 61 70 3eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( 1r ‘ 𝐴 ) , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 1r ‘ 𝑄 ) )
72 15 22 71 3eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 1r ‘ 𝑄 ) )