Theorem pm2mpf1o

Description: The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-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	pm2mpf1o	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-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	pm2mpf1	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> L )
12	1 2 3 4 5 6 7 8 9 10	pm2mpfo	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -onto-> L )
13		df-f1o	|- ( T : B -1-1-onto-> L <-> ( T : B -1-1-> L /\ T : B -onto-> L ) )
14	11 12 13	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-onto-> L )