mat2pmatscmxcl

Description: A transformed matrix multiplied with a power of the variable of a polynomial is a polynomial matrix. (Contributed by AV, 6-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatscmxcl.a	$⊢ A = N Mat R$
	mat2pmatscmxcl.k	$⊢ K = {Base}_{A}$
	mat2pmatscmxcl.t	$⊢ T = N matToPolyMat R$
	mat2pmatscmxcl.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatscmxcl.c	$⊢ C = N Mat P$
	mat2pmatscmxcl.b	$⊢ B = {Base}_{C}$
	mat2pmatscmxcl.m	$⊢ \underset{˙}{*} = \cdot_{C}$
	mat2pmatscmxcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	mat2pmatscmxcl.x	$⊢ X = {var}_{1} (R)$
Assertion	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to (L \underset{˙}{\times} X) \underset{˙}{*} T (M) \in B$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatscmxcl.a	$⊢ A = N Mat R$
2		mat2pmatscmxcl.k	$⊢ K = {Base}_{A}$
3		mat2pmatscmxcl.t	$⊢ T = N matToPolyMat R$
4		mat2pmatscmxcl.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatscmxcl.c	$⊢ C = N Mat P$
6		mat2pmatscmxcl.b	$⊢ B = {Base}_{C}$
7		mat2pmatscmxcl.m	$⊢ \underset{˙}{*} = \cdot_{C}$
8		mat2pmatscmxcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
9		mat2pmatscmxcl.x	$⊢ X = {var}_{1} (R)$
10		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to N \in Fin$
11	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
12	11	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to P \in Ring$
13		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15	4 9 13 8 14	ply1moncl	$⊢ (R \in Ring \land L \in ℕ_{0}) \to L \underset{˙}{\times} X \in {Base}_{P}$
16	15	ad2ant2l	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to L \underset{˙}{\times} X \in {Base}_{P}$
17		simpl	$⊢ (M \in K \land L \in ℕ_{0}) \to M \in K$
18	17	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to ((N \in Fin \land R \in Ring) \land M \in K)$
19		df-3an	$⊢ (N \in Fin \land R \in Ring \land M \in K) \leftrightarrow ((N \in Fin \land R \in Ring) \land M \in K)$
20	18 19	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to (N \in Fin \land R \in Ring \land M \in K)$
21	3 1 2 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to T (M) \in B$
22	20 21	syl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to T (M) \in B$
23	14 5 6 7	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (L \underset{˙}{\times} X \in {Base}_{P} \land T (M) \in B)) \to (L \underset{˙}{\times} X) \underset{˙}{*} T (M) \in B$
24	10 12 16 22 23	syl22anc	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to (L \underset{˙}{\times} X) \underset{˙}{*} T (M) \in B$

Metamath Proof Explorer

Theorem mat2pmatscmxcl

Proof