Theorem mat2pmatbas

Description: The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 1-Aug-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
7	1 2 3 4 6	mat2pmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
10		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
11	4	fvexi	⊢ 𝑃 ∈ V
12	11	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ V )
13		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
14	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	14	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
16	15	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑃 ∈ Ring )
17	4	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
18	17	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ LMod )
19	18	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑃 ∈ LMod )
20		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
21	6 13 16 19 20 8	asclf	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
22	4	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
23	22	fveq2d	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
24	23	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
25	24	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
26	25	feq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) ↔ ( algSc ‘ 𝑃 ) : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) ) )
27	21 26	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
28		simp2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
29		simp3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
30	3	eleq2i	⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
31	30	biimpi	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
32	31	3ad2ant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
33	32	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
34		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35	2 34	matecl	⊢ ( ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
36	28 29 33 35	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
37	27 36	ffvelrnd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑀 𝑦 ) ) ∈ ( Base ‘ 𝑃 ) )
38	5 8 9 10 12 37	matbas2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) ∈ ( Base ‘ 𝐶 ) )
39	7 38	eqeltrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐶 ) )