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	|- P = ( Poly1 ` R )
	pm2mpval.c	|- C = ( N Mat P )
	pm2mpval.b	|- B = ( Base ` C )
	pm2mpval.m	|- .* = ( .s ` Q )
	pm2mpval.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
	pm2mpval.x	|- X = ( var1 ` A )
	pm2mpval.a	|- A = ( N Mat R )
	pm2mpval.q	|- Q = ( Poly1 ` A )
	pm2mpval.t	|- T = ( N pMatToMatPoly R )
Assertion	idpm2idmp	|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` C ) ) = ( 1r ` Q ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	|- P = ( Poly1 ` R )
2		pm2mpval.c	|- C = ( N Mat P )
3		pm2mpval.b	|- B = ( Base ` C )
4		pm2mpval.m	|- .* = ( .s ` Q )
5		pm2mpval.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
6		pm2mpval.x	|- X = ( var1 ` A )
7		pm2mpval.a	|- A = ( N Mat R )
8		pm2mpval.q	|- Q = ( Poly1 ` A )
9		pm2mpval.t	|- T = ( N pMatToMatPoly R )
10	1 2	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
11		eqid	|- ( 1r ` C ) = ( 1r ` C )
12	3 11	ringidcl	|- ( C e. Ring -> ( 1r ` C ) e. B )
13	10 12	syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. B )
14	1 2 3 4 5 6 7 8 9	pm2mpfval	|- ( ( N e. Fin /\ R e. Ring /\ ( 1r ` C ) e. B ) -> ( T ` ( 1r ` C ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( 1r ` C ) decompPMat k ) .* ( k .^ X ) ) ) ) )
15	13 14	mpd3an3	|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` C ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( 1r ` C ) decompPMat k ) .* ( k .^ X ) ) ) ) )
16		eqid	|- ( 0g ` A ) = ( 0g ` A )
17		eqid	|- ( 1r ` A ) = ( 1r ` A )
18	1 2 11 7 16 17	decpmatid	|- ( ( N e. Fin /\ R e. Ring /\ k e. NN0 ) -> ( ( 1r ` C ) decompPMat k ) = if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) )
19	18	3expa	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 1r ` C ) decompPMat k ) = if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) )
20	19	oveq1d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( ( 1r ` C ) decompPMat k ) .* ( k .^ X ) ) = ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) )
21	20	mpteq2dva	|- ( ( N e. Fin /\ R e. Ring ) -> ( k e. NN0 |-> ( ( ( 1r ` C ) decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) ) )
22	21	oveq2d	|- ( ( N e. Fin /\ R e. Ring ) -> ( Q gsum ( k e. NN0 |-> ( ( ( 1r ` C ) decompPMat k ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) ) ) )
23		ovif	|- ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) = if ( k = 0 , ( ( 1r ` A ) .* ( k .^ X ) ) , ( ( 0g ` A ) .* ( k .^ X ) ) )
24	7	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
25	8	ply1sca	|- ( A e. Ring -> A = ( Scalar ` Q ) )
26	24 25	syl	|- ( ( N e. Fin /\ R e. Ring ) -> A = ( Scalar ` Q ) )
27	26	adantr	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> A = ( Scalar ` Q ) )
28	27	fveq2d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( 1r ` A ) = ( 1r ` ( Scalar ` Q ) ) )
29	28	oveq1d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 1r ` A ) .* ( k .^ X ) ) = ( ( 1r ` ( Scalar ` Q ) ) .* ( k .^ X ) ) )
30	8	ply1lmod	|- ( A e. Ring -> Q e. LMod )
31	24 30	syl	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
32		eqid	|- ( mulGrp ` Q ) = ( mulGrp ` Q )
33		eqid	|- ( Base ` Q ) = ( Base ` Q )
34	8 6 32 5 33	ply1moncl	|- ( ( A e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
35	24 34	sylan	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
36		eqid	|- ( Scalar ` Q ) = ( Scalar ` Q )
37		eqid	|- ( 1r ` ( Scalar ` Q ) ) = ( 1r ` ( Scalar ` Q ) )
38	33 36 4 37	lmodvs1	|- ( ( Q e. LMod /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( ( 1r ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( k .^ X ) )
39	31 35 38	syl2an2r	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 1r ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( k .^ X ) )
40	29 39	eqtrd	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 1r ` A ) .* ( k .^ X ) ) = ( k .^ X ) )
41	27	fveq2d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( 0g ` A ) = ( 0g ` ( Scalar ` Q ) ) )
42	41	oveq1d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 0g ` A ) .* ( k .^ X ) ) = ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) )
43		eqid	|- ( 0g ` ( Scalar ` Q ) ) = ( 0g ` ( Scalar ` Q ) )
44		eqid	|- ( 0g ` Q ) = ( 0g ` Q )
45	33 36 4 43 44	lmod0vs	|- ( ( Q e. LMod /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
46	31 35 45	syl2an2r	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
47	42 46	eqtrd	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( ( 0g ` A ) .* ( k .^ X ) ) = ( 0g ` Q ) )
48	40 47	ifeq12d	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> if ( k = 0 , ( ( 1r ` A ) .* ( k .^ X ) ) , ( ( 0g ` A ) .* ( k .^ X ) ) ) = if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) )
49	23 48	eqtrid	|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. NN0 ) -> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) = if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) )
50	49	mpteq2dva	|- ( ( N e. Fin /\ R e. Ring ) -> ( k e. NN0 |-> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) ) )
51	50	oveq2d	|- ( ( N e. Fin /\ R e. Ring ) -> ( Q gsum ( k e. NN0 |-> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 |-> if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) ) ) )
52	8	ply1ring	|- ( A e. Ring -> Q e. Ring )
53		ringmnd	|- ( Q e. Ring -> Q e. Mnd )
54	24 52 53	3syl	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. Mnd )
55		nn0ex	|- NN0 e. _V
56	55	a1i	|- ( ( N e. Fin /\ R e. Ring ) -> NN0 e. _V )
57		0nn0	|- 0 e. NN0
58	57	a1i	|- ( ( N e. Fin /\ R e. Ring ) -> 0 e. NN0 )
59		eqid	|- ( k e. NN0 |-> if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) )
60	35	ralrimiva	|- ( ( N e. Fin /\ R e. Ring ) -> A. k e. NN0 ( k .^ X ) e. ( Base ` Q ) )
61	44 54 56 58 59 60	gsummpt1n0	|- ( ( N e. Fin /\ R e. Ring ) -> ( Q gsum ( k e. NN0 |-> if ( k = 0 , ( k .^ X ) , ( 0g ` Q ) ) ) ) = [_ 0 / k ]_ ( k .^ X ) )
62		c0ex	|- 0 e. _V
63		csbov1g	|- ( 0 e. _V -> [_ 0 / k ]_ ( k .^ X ) = ( [_ 0 / k ]_ k .^ X ) )
64	62 63	mp1i	|- ( ( N e. Fin /\ R e. Ring ) -> [_ 0 / k ]_ ( k .^ X ) = ( [_ 0 / k ]_ k .^ X ) )
65		csbvarg	|- ( 0 e. _V -> [_ 0 / k ]_ k = 0 )
66	62 65	mp1i	|- ( ( N e. Fin /\ R e. Ring ) -> [_ 0 / k ]_ k = 0 )
67	66	oveq1d	|- ( ( N e. Fin /\ R e. Ring ) -> ( [_ 0 / k ]_ k .^ X ) = ( 0 .^ X ) )
68	8 6 32 5	ply1idvr1	|- ( A e. Ring -> ( 0 .^ X ) = ( 1r ` Q ) )
69	24 68	syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0 .^ X ) = ( 1r ` Q ) )
70	64 67 69	3eqtrd	|- ( ( N e. Fin /\ R e. Ring ) -> [_ 0 / k ]_ ( k .^ X ) = ( 1r ` Q ) )
71	51 61 70	3eqtrd	|- ( ( N e. Fin /\ R e. Ring ) -> ( Q gsum ( k e. NN0 |-> ( if ( k = 0 , ( 1r ` A ) , ( 0g ` A ) ) .* ( k .^ X ) ) ) ) = ( 1r ` Q ) )
72	15 22 71	3eqtrd	|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` C ) ) = ( 1r ` Q ) )