mat2pmatbas

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

	Ref	Expression
Hypotheses	mat2pmatbas.t	$⊢ T = N matToPolyMat R$
	mat2pmatbas.a	$⊢ A = N Mat R$
	mat2pmatbas.b	$⊢ B = {Base}_{A}$
	mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatbas.c	$⊢ C = N Mat P$
Assertion	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{C}$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$⊢ T = N matToPolyMat R$
2		mat2pmatbas.a	$⊢ A = N Mat R$
3		mat2pmatbas.b	$⊢ B = {Base}_{A}$
4		mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatbas.c	$⊢ C = N Mat P$
6		eqid	$⊢ algSc (P) = algSc (P)$
7	1 2 3 4 6	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) = (x \in N, y \in N ⟼ algSc (P) (x M y))$
8		eqid	$⊢ {Base}_{P} = {Base}_{P}$
9		eqid	$⊢ {Base}_{C} = {Base}_{C}$
10		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to N \in Fin$
11	4	fvexi	$⊢ P \in V$
12	11	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in V$
13		eqid	$⊢ Scalar (P) = Scalar (P)$
14	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	14	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in Ring$
16	15	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to P \in Ring$
17	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
18	17	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in LMod$
19	18	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to P \in LMod$
20		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
21	6 13 16 19 20 8	asclf	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to algSc (P) : {Base}_{Scalar (P)} ⟶ {Base}_{P}$
22	4	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
23	22	fveq2d	$⊢ R \in Ring \to {Base}_{R} = {Base}_{Scalar (P)}$
24	23	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {Base}_{R} = {Base}_{Scalar (P)}$
25	24	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to {Base}_{R} = {Base}_{Scalar (P)}$
26	25	feq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to (algSc (P) : {Base}_{R} ⟶ {Base}_{P} \leftrightarrow algSc (P) : {Base}_{Scalar (P)} ⟶ {Base}_{P})$
27	21 26	mpbird	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
28		simp2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to x \in N$
29		simp3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to y \in N$
30	3	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
31	30	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
32	31	3ad2ant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M \in {Base}_{A}$
33	32	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to M \in {Base}_{A}$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35	2 34	matecl	$⊢ (x \in N \land y \in N \land M \in {Base}_{A}) \to x M y \in {Base}_{R}$
36	28 29 33 35	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to x M y \in {Base}_{R}$
37	27 36	ffvelrnd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in N \land y \in N) \to algSc (P) (x M y) \in {Base}_{P}$
38	5 8 9 10 12 37	matbas2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (x \in N, y \in N ⟼ algSc (P) (x M y)) \in {Base}_{C}$
39	7 38	eqeltrd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{C}$

Metamath Proof Explorer

Theorem mat2pmatbas

Proof