Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpfo.p	|- P = ( Poly1 ` R )
	pm2mpfo.c	|- C = ( N Mat P )
	pm2mpfo.b	|- B = ( Base ` C )
	pm2mpfo.m	|- .* = ( .s ` Q )
	pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
	pm2mpfo.x	|- X = ( var1 ` A )
	pm2mpfo.a	|- A = ( N Mat R )
	pm2mpfo.q	|- Q = ( Poly1 ` A )
	pm2mpfo.l	|- L = ( Base ` Q )
	pm2mpfo.t	|- T = ( N pMatToMatPoly R )
Assertion	pm2mpfo	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -onto-> L )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	|- P = ( Poly1 ` R )
2		pm2mpfo.c	|- C = ( N Mat P )
3		pm2mpfo.b	|- B = ( Base ` C )
4		pm2mpfo.m	|- .* = ( .s ` Q )
5		pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
6		pm2mpfo.x	|- X = ( var1 ` A )
7		pm2mpfo.a	|- A = ( N Mat R )
8		pm2mpfo.q	|- Q = ( Poly1 ` A )
9		pm2mpfo.l	|- L = ( Base ` Q )
10		pm2mpfo.t	|- T = ( N pMatToMatPoly R )
11	1 2 3 4 5 6 7 8 10 9	pm2mpf	|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )
12		eqid	|- ( .s ` P ) = ( .s ` P )
13		eqid	|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
14		eqid	|- ( var1 ` R ) = ( var1 ` R )
15		eqid	|- ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) = ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) )
16	7 8 9 12 13 14 15 1 10	mp2pm2mp	|- ( ( N e. Fin /\ R e. Ring /\ p e. L ) -> ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p )
17	16	3expa	|- ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p )
18	7 8 9 1 12 13 14 15 2 3	mply1topmatcl	|- ( ( N e. Fin /\ R e. Ring /\ p e. L ) -> ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) e. B )
19	18	3expa	|- ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) e. B )
20		simpr	|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) )
21	20	fveq2d	|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( T ` f ) = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) )
22	21	eqeq2d	|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( p = ( T ` f ) <-> p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) ) )
23	19 22	rspcedv	|- ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> E. f e. B p = ( T ` f ) ) )
24	23	com12	|- ( p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) ) )
25	24	eqcoms	|- ( ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p -> ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) ) )
26	17 25	mpcom	|- ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) )
27	26	ralrimiva	|- ( ( N e. Fin /\ R e. Ring ) -> A. p e. L E. f e. B p = ( T ` f ) )
28		dffo3	|- ( T : B -onto-> L <-> ( T : B --> L /\ A. p e. L E. f e. B p = ( T ` f ) ) )
29	11 27 28	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -onto-> L )