Theorem m2cpmfo

Description: The matrix transformation is a function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	m2cpmfo.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpmfo.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	m2cpmfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpmfo.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
Assertion	m2cpmfo	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –onto→ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		m2cpmfo.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpmfo.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3		m2cpmfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2cpmfo.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
5	1 2 3 4	m2cpmf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 ⟶ 𝑆 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		simplll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) → 𝑁 ∈ Fin )
8		simpllr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) → 𝑅 ∈ Ring )
9		eqid	⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
10		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
11		eqid	⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
12		simp2	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
13		simp3	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
14		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
15	1 14 9 11	cpmatpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
16	15	ad4ant124	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
17	16	3ad2ant1	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
18	9 10 11 12 13 17	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑚 𝑗 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
19		0nn0	⊢ 0 ∈ ℕ0
20		eqid	⊢ ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) )
21	20 10 14 6	coe1fvalcl	⊢ ( ( ( 𝑖 𝑚 𝑗 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
22	18 19 21	sylancl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
23	3 6 4 7 8 22	matbas2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ∈ 𝐾 )
24	23	fmpttd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) : 𝑆 ⟶ 𝐾 )
25		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
26	24 25	ffvelrnd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ∈ 𝐾 )
27		fveq2	⊢ ( 𝑐 = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) → ( 𝑇 ‘ 𝑐 ) = ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) )
28	27	eqeq2d	⊢ ( 𝑐 = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) → ( 𝑥 = ( 𝑇 ‘ 𝑐 ) ↔ 𝑥 = ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) ) )
29	28	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑐 = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) → ( 𝑥 = ( 𝑇 ‘ 𝑐 ) ↔ 𝑥 = ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) ) )
30		eqid	⊢ ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑁 cPolyMatToMat 𝑅 )
31	30 1	cpm2mfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) )
32	31	fveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) )
33	32	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) )
34	33	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) = ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ 𝑥 ) )
35	34	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) = ( 𝑇 ‘ ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ 𝑥 ) ) )
36	1 30 2	m2cpminvid2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 ‘ ( ( 𝑁 cPolyMatToMat 𝑅 ) ‘ 𝑥 ) ) = 𝑥 )
37	35 36	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) = 𝑥 )
38	37	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) = 𝑥 )
39	38	eqcomd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = ( 𝑇 ‘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 0 ) ) ) ‘ 𝑥 ) ) )
40	26 29 39	rspcedvd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑐 ∈ 𝐾 𝑥 = ( 𝑇 ‘ 𝑐 ) )
41	40	ralrimiva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑐 ∈ 𝐾 𝑥 = ( 𝑇 ‘ 𝑐 ) )
42		dffo3	⊢ ( 𝑇 : 𝐾 –onto→ 𝑆 ↔ ( 𝑇 : 𝐾 ⟶ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∃ 𝑐 ∈ 𝐾 𝑥 = ( 𝑇 ‘ 𝑐 ) ) )
43	5 41 42	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –onto→ 𝑆 )