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	syl5eq	⊢ ( ( ( 𝑁 ∈ 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 ‘ 𝑄 ) )