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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpfo.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	pm2mpfo.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	pm2mpf1o	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1-onto→ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		pm2mpfo.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
10		pm2mpfo.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
11	1 2 3 4 5 6 7 8 10 9	pm2mpf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐿 )
12	1 2 3 4 5 6 7 8 9 10	pm2mpfo	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –onto→ 𝐿 )
13		df-f1o	⊢ ( 𝑇 : 𝐵 –1-1-onto→ 𝐿 ↔ ( 𝑇 : 𝐵 –1-1→ 𝐿 ∧ 𝑇 : 𝐵 –onto→ 𝐿 ) )
14	11 12 13	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1-onto→ 𝐿 )