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	⊢ 𝑃 = ( 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	pm2mpfo	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –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	pm2mpf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐿 )
12		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
13		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
14		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
15		eqid	⊢ ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) = ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
16	7 8 9 12 13 14 15 1 10	mp2pm2mp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑝 ∈ 𝐿 ) → ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 )
17	16	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 )
18	7 8 9 1 12 13 14 15 2 3	mply1topmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑝 ∈ 𝐿 ) → ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ∈ 𝐵 )
19	18	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ∈ 𝐵 )
20		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) ∧ 𝑓 = ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → 𝑓 = ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) )
21	20	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) ∧ 𝑓 = ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( 𝑇 ‘ 𝑓 ) = ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) )
22	21	eqeq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) ∧ 𝑓 = ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( 𝑝 = ( 𝑇 ‘ 𝑓 ) ↔ 𝑝 = ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) ) )
23	19 22	rspcedv	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ( 𝑝 = ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) ) )
24	23	com12	⊢ ( 𝑝 = ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) ) )
25	24	eqcoms	⊢ ( ( 𝑇 ‘ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) ) )
26	17 25	mpcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝 ∈ 𝐿 ) → ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) )
27	26	ralrimiva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑝 ∈ 𝐿 ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) )
28		dffo3	⊢ ( 𝑇 : 𝐵 –onto→ 𝐿 ↔ ( 𝑇 : 𝐵 ⟶ 𝐿 ∧ ∀ 𝑝 ∈ 𝐿 ∃ 𝑓 ∈ 𝐵 𝑝 = ( 𝑇 ‘ 𝑓 ) ) )
29	11 27 28	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –onto→ 𝐿 )