mply1topmatcl

Description: A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Hypotheses	mply1topmat.a	\|- A = ( N Mat R )
	mply1topmat.q	\|- Q = ( Poly1 ` A )
	mply1topmat.l	\|- L = ( Base ` Q )
	mply1topmat.p	\|- P = ( Poly1 ` R )
	mply1topmat.m	\|- .x. = ( .s ` P )
	mply1topmat.e	\|- E = ( .g ` ( mulGrp ` P ) )
	mply1topmat.y	\|- Y = ( var1 ` R )
	mply1topmat.i	\|- I = ( p e. L \|-> ( i e. N , j e. N \|-> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
	mply1topmatcl.c	\|- C = ( N Mat P )
	mply1topmatcl.b	\|- B = ( Base ` C )
Assertion	mply1topmatcl	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	\|- A = ( N Mat R )
2		mply1topmat.q	\|- Q = ( Poly1 ` A )
3		mply1topmat.l	\|- L = ( Base ` Q )
4		mply1topmat.p	\|- P = ( Poly1 ` R )
5		mply1topmat.m	\|- .x. = ( .s ` P )
6		mply1topmat.e	\|- E = ( .g ` ( mulGrp ` P ) )
7		mply1topmat.y	\|- Y = ( var1 ` R )
8		mply1topmat.i	\|- I = ( p e. L \|-> ( i e. N , j e. N \|-> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
9		mply1topmatcl.c	\|- C = ( N Mat P )
10		mply1topmatcl.b	\|- B = ( Base ` C )
11	1 2 3 4 5 6 7 8	mply1topmatval	\|- ( ( N e. Fin /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N \|-> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
12	11	3adant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N \|-> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
13		eqid	\|- ( Base ` P ) = ( Base ` P )
14		simp1	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> N e. Fin )
15	4	fvexi	\|- P e. _V
16	15	a1i	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. _V )
17		eqid	\|- ( 0g ` P ) = ( 0g ` P )
18	4	ply1ring	\|- ( R e. Ring -> P e. Ring )
19		ringcmn	\|- ( P e. Ring -> P e. CMnd )
20	18 19	syl	\|- ( R e. Ring -> P e. CMnd )
21	20	3ad2ant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. CMnd )
22	21	3ad2ant1	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> P e. CMnd )
23		nn0ex	\|- NN0 e. _V
24	23	a1i	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> NN0 e. _V )
25	4	ply1lmod	\|- ( R e. Ring -> P e. LMod )
26	25	3ad2ant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
27	26	3ad2ant1	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> P e. LMod )
28	27	adantr	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> P e. LMod )
29		eqid	\|- ( Base ` R ) = ( Base ` R )
30		eqid	\|- ( Base ` A ) = ( Base ` A )
31		simpl2	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> i e. N )
32		simpl3	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> j e. N )
33		simpl13	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> O e. L )
34		eqid	\|- ( coe1 ` O ) = ( coe1 ` O )
35	34 3 2 30	coe1f	\|- ( O e. L -> ( coe1 ` O ) : NN0 --> ( Base ` A ) )
36	33 35	syl	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( coe1 ` O ) : NN0 --> ( Base ` A ) )
37		simpr	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> k e. NN0 )
38	36 37	ffvelrnd	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
39	1 29 30 31 32 38	matecld	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` R ) )
40	4	ply1sca	\|- ( R e. Ring -> R = ( Scalar ` P ) )
41	40	eqcomd	\|- ( R e. Ring -> ( Scalar ` P ) = R )
42	41	3ad2ant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( Scalar ` P ) = R )
43	42	fveq2d	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
44	43	3ad2ant1	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
45	44	adantr	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
46	39 45	eleqtrrd	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` ( Scalar ` P ) ) )
47	18	3ad2ant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. Ring )
48		eqid	\|- ( mulGrp ` P ) = ( mulGrp ` P )
49	48	ringmgp	\|- ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
50	47 49	syl	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( mulGrp ` P ) e. Mnd )
51	50	3ad2ant1	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( mulGrp ` P ) e. Mnd )
52	51	adantr	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
53	7 4 13	vr1cl	\|- ( R e. Ring -> Y e. ( Base ` P ) )
54	53	3ad2ant2	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> Y e. ( Base ` P ) )
55	54	3ad2ant1	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> Y e. ( Base ` P ) )
56	55	adantr	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> Y e. ( Base ` P ) )
57	48 13	mgpbas	\|- ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
58	57 6	mulgnn0cl	\|- ( ( ( mulGrp ` P ) e. Mnd /\ k e. NN0 /\ Y e. ( Base ` P ) ) -> ( k E Y ) e. ( Base ` P ) )
59	52 37 56 58	syl3anc	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( k E Y ) e. ( Base ` P ) )
60		eqid	\|- ( Scalar ` P ) = ( Scalar ` P )
61		eqid	\|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
62	13 60 5 61	lmodvscl	\|- ( ( P e. LMod /\ ( i ( ( coe1 ` O ) ` k ) j ) e. ( Base ` ( Scalar ` P ) ) /\ ( k E Y ) e. ( Base ` P ) ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
63	28 46 59 62	syl3anc	\|- ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) /\ k e. NN0 ) -> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) e. ( Base ` P ) )
64	63	fmpttd	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) : NN0 --> ( Base ` P ) )
65	1 2 3 4 5 6 7	mply1topmatcllem	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) finSupp ( 0g ` P ) )
66	13 17 22 24 64 65	gsumcl	\|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ i e. N /\ j e. N ) -> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) e. ( Base ` P ) )
67	9 13 10 14 16 66	matbas2d	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N \|-> ( P gsum ( k e. NN0 \|-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. B )
68	12 67	eqeltrd	\|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) e. B )

Metamath Proof Explorer

Theorem mply1topmatcl

Proof