Metamath Proof Explorer

Theorem cpmatsrgpmat

Description: The set of all constant polynomial matrices over a ring R is a subring of the ring of all polynomial matrices over the ring R . (Contributed by AV, 18-Nov-2019)

		Ref	Expression
	Hypotheses	cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
		cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
		cpmatsrngpmat.c	$⊢ C = N Mat P$
	Assertion	cpmatsrgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (C)$

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
2		cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
3		cpmatsrngpmat.c	$⊢ C = N Mat P$
4	1 2 3	cpmatsubgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (C)$
5	1 2 3	1elcpmat	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in S$
6	1 2 3	cpmatmcl	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x \cdot_{C} y \in S$
7	2 3	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		eqid	$⊢ 1_{C} = 1_{C}$
10		eqid	$⊢ \cdot_{C} = \cdot_{C}$
11	8 9 10	issubrg2	$⊢ C \in Ring \to (S \in SubRing (C) \leftrightarrow (S \in SubGrp (C) \land 1_{C} \in S \land \forall x \in S \forall y \in S x \cdot_{C} y \in S))$
12	7 11	syl	$⊢ (N \in Fin \land R \in Ring) \to (S \in SubRing (C) \leftrightarrow (S \in SubGrp (C) \land 1_{C} \in S \land \forall x \in S \forall y \in S x \cdot_{C} y \in S))$
13	4 5 6 12	mpbir3and	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (C)$