cpmatacl

Description: The set of all constant polynomial matrices over a ring R is closed under addition. (Contributed by AV, 17-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

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

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		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ algSc (P) = algSc (P)$
7	1 2 3 4 5 6	cpmatelimp2	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)))$
8	1 2 3 4 5 6	cpmatelimp2	$⊢ (N \in Fin \land R \in Ring) \to (y \in S \to (y \in {Base}_{C} \land \forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b)))$
9		r19.26-2	$⊢ \forall i \in N \forall j \in N (\exists a \in {Base}_{R} i x j = algSc (P) (a) \land \exists b \in {Base}_{R} i y j = algSc (P) (b)) \leftrightarrow (\forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a) \land \forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b))$
10		eqid	$⊢ +_{R} = +_{R}$
11	5 10	ringacl	$⊢ (R \in Ring \land a \in {Base}_{R} \land b \in {Base}_{R}) \to a +_{R} b \in {Base}_{R}$
12	11	3expb	$⊢ (R \in Ring \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to a +_{R} b \in {Base}_{R}$
13	2	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
14	13	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
15	14	fveq2d	$⊢ R \in Ring \to +_{Scalar (P)} = +_{R}$
16	15	oveqd	$⊢ R \in Ring \to a +_{Scalar (P)} b = a +_{R} b$
17	16	eleq1d	$⊢ R \in Ring \to (a +_{Scalar (P)} b \in {Base}_{R} \leftrightarrow a +_{R} b \in {Base}_{R})$
18	17	adantr	$⊢ (R \in Ring \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to (a +_{Scalar (P)} b \in {Base}_{R} \leftrightarrow a +_{R} b \in {Base}_{R})$
19	12 18	mpbird	$⊢ (R \in Ring \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to a +_{Scalar (P)} b \in {Base}_{R}$
20	19	ad5ant25	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to a +_{Scalar (P)} b \in {Base}_{R}$
21	20	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to a +_{Scalar (P)} b \in {Base}_{R}$
22		fveq2	$⊢ c = a +_{Scalar (P)} b \to algSc (P) (c) = algSc (P) (a +_{Scalar (P)} b)$
23	22	eqeq2d	$⊢ c = a +_{Scalar (P)} b \to (i (x +_{C} y) j = algSc (P) (c) \leftrightarrow i (x +_{C} y) j = algSc (P) (a +_{Scalar (P)} b))$
24	23	adantl	$⊢ ((((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \land c = a +_{Scalar (P)} b) \to (i (x +_{C} y) j = algSc (P) (c) \leftrightarrow i (x +_{C} y) j = algSc (P) (a +_{Scalar (P)} b))$
25		simpr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \to (y \in {Base}_{C} \land x \in {Base}_{C})$
26	25	ancomd	$⊢ ((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \to (x \in {Base}_{C} \land y \in {Base}_{C})$
27	26	anim1i	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (i \in N \land j \in N))$
28	27	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (i \in N \land j \in N))$
29		eqid	$⊢ +_{C} = +_{C}$
30		eqid	$⊢ +_{P} = +_{P}$
31	3 4 29 30	matplusgcell	$⊢ ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (i \in N \land j \in N)) \to i (x +_{C} y) j = (i x j) +_{P} (i y j)$
32	28 31	syl	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to i (x +_{C} y) j = (i x j) +_{P} (i y j)$
33		oveq12	$⊢ (i x j = algSc (P) (a) \land i y j = algSc (P) (b)) \to (i x j) +_{P} (i y j) = algSc (P) (a) +_{P} algSc (P) (b)$
34	33	ancoms	$⊢ (i y j = algSc (P) (b) \land i x j = algSc (P) (a)) \to (i x j) +_{P} (i y j) = algSc (P) (a) +_{P} algSc (P) (b)$
35		eqid	$⊢ Scalar (P) = Scalar (P)$
36	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
37	36	ad4antlr	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to P \in Ring$
38	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
39	38	ad4antlr	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to P \in LMod$
40	6 35 37 39	asclghm	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to algSc (P) \in (Scalar (P) GrpHom P)$
41	13	adantl	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (P)$
42	41	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{Scalar (P)}$
43	42	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (a \in {Base}_{R} \leftrightarrow a \in {Base}_{Scalar (P)})$
44	43	biimpd	$⊢ (N \in Fin \land R \in Ring) \to (a \in {Base}_{R} \to a \in {Base}_{Scalar (P)})$
45	44	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to (a \in {Base}_{R} \to a \in {Base}_{Scalar (P)})$
46	45	adantrd	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to ((a \in {Base}_{R} \land b \in {Base}_{R}) \to a \in {Base}_{Scalar (P)})$
47	46	imp	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to a \in {Base}_{Scalar (P)}$
48	13	ad3antlr	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to R = Scalar (P)$
49	48	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to {Base}_{R} = {Base}_{Scalar (P)}$
50	49	eleq2d	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to (b \in {Base}_{R} \leftrightarrow b \in {Base}_{Scalar (P)})$
51	50	biimpd	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to (b \in {Base}_{R} \to b \in {Base}_{Scalar (P)})$
52	51	adantld	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to ((a \in {Base}_{R} \land b \in {Base}_{R}) \to b \in {Base}_{Scalar (P)})$
53	52	imp	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to b \in {Base}_{Scalar (P)}$
54		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
55		eqid	$⊢ +_{Scalar (P)} = +_{Scalar (P)}$
56	54 55 30	ghmlin	$⊢ (algSc (P) \in (Scalar (P) GrpHom P) \land a \in {Base}_{Scalar (P)} \land b \in {Base}_{Scalar (P)}) \to algSc (P) (a +_{Scalar (P)} b) = algSc (P) (a) +_{P} algSc (P) (b)$
57	40 47 53 56	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to algSc (P) (a +_{Scalar (P)} b) = algSc (P) (a) +_{P} algSc (P) (b)$
58	57	eqcomd	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to algSc (P) (a) +_{P} algSc (P) (b) = algSc (P) (a +_{Scalar (P)} b)$
59	34 58	sylan9eqr	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to (i x j) +_{P} (i y j) = algSc (P) (a +_{Scalar (P)} b)$
60	32 59	eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to i (x +_{C} y) j = algSc (P) (a +_{Scalar (P)} b)$
61	21 24 60	rspcedvd	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \land (i y j = algSc (P) (b) \land i x j = algSc (P) (a))) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)$
62	61	exp32	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to (i y j = algSc (P) (b) \to (i x j = algSc (P) (a) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
63	62	anassrs	$⊢ (((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \to (i y j = algSc (P) (b) \to (i x j = algSc (P) (a) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
64	63	rexlimdva	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to (\exists b \in {Base}_{R} i y j = algSc (P) (b) \to (i x j = algSc (P) (a) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
65	64	com23	$⊢ ((((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to (i x j = algSc (P) (a) \to (\exists b \in {Base}_{R} i y j = algSc (P) (b) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
66	65	rexlimdva	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to (\exists a \in {Base}_{R} i x j = algSc (P) (a) \to (\exists b \in {Base}_{R} i y j = algSc (P) (b) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
67	66	impd	$⊢ (((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \land (i \in N \land j \in N)) \to ((\exists a \in {Base}_{R} i x j = algSc (P) (a) \land \exists b \in {Base}_{R} i y j = algSc (P) (b)) \to \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))$
68	67	ralimdvva	$⊢ ((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \to (\forall i \in N \forall j \in N (\exists a \in {Base}_{R} i x j = algSc (P) (a) \land \exists b \in {Base}_{R} i y j = algSc (P) (b)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))$
69	9 68	syl5bir	$⊢ ((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \to ((\forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a) \land \forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))$
70	69	expd	$⊢ ((N \in Fin \land R \in Ring) \land (y \in {Base}_{C} \land x \in {Base}_{C})) \to (\forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a) \to (\forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
71	70	expr	$⊢ ((N \in Fin \land R \in Ring) \land y \in {Base}_{C}) \to (x \in {Base}_{C} \to (\forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a) \to (\forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))))$
72	71	impd	$⊢ ((N \in Fin \land R \in Ring) \land y \in {Base}_{C}) \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to (\forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
73	72	ex	$⊢ (N \in Fin \land R \in Ring) \to (y \in {Base}_{C} \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to (\forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))))$
74	73	com34	$⊢ (N \in Fin \land R \in Ring) \to (y \in {Base}_{C} \to (\forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b) \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))))$
75	74	impd	$⊢ (N \in Fin \land R \in Ring) \to ((y \in {Base}_{C} \land \forall i \in N \forall j \in N \exists b \in {Base}_{R} i y j = algSc (P) (b)) \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
76	8 75	syld	$⊢ (N \in Fin \land R \in Ring) \to (y \in S \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
77	76	com23	$⊢ (N \in Fin \land R \in Ring) \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to (y \in S \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
78	7 77	syld	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (y \in S \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)))$
79	78	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c)$
80		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
81	80	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to N \in Fin$
82		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
83	82	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to R \in Ring$
84	2 3	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
85	84	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to C \in Ring$
86		simpl	$⊢ (x \in S \land y \in S) \to x \in S$
87	86	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to ((N \in Fin \land R \in Ring) \land x \in S)$
88		df-3an	$⊢ (N \in Fin \land R \in Ring \land x \in S) \leftrightarrow ((N \in Fin \land R \in Ring) \land x \in S)$
89	87 88	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (N \in Fin \land R \in Ring \land x \in S)$
90	1 2 3 4	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to x \in {Base}_{C}$
91	89 90	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \in {Base}_{C}$
92		simpr	$⊢ (x \in S \land y \in S) \to y \in S$
93	92	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to ((N \in Fin \land R \in Ring) \land y \in S)$
94		df-3an	$⊢ (N \in Fin \land R \in Ring \land y \in S) \leftrightarrow ((N \in Fin \land R \in Ring) \land y \in S)$
95	93 94	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (N \in Fin \land R \in Ring \land y \in S)$
96	1 2 3 4	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land y \in S) \to y \in {Base}_{C}$
97	95 96	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to y \in {Base}_{C}$
98	4 29	ringacl	$⊢ (C \in Ring \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x +_{C} y \in {Base}_{C}$
99	85 91 97 98	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x +_{C} y \in {Base}_{C}$
100	1 2 3 4 5 6	cpmatel2	$⊢ (N \in Fin \land R \in Ring \land x +_{C} y \in {Base}_{C}) \to (x +_{C} y \in S \leftrightarrow \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))$
101	81 83 99 100	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (x +_{C} y \in S \leftrightarrow \forall i \in N \forall j \in N \exists c \in {Base}_{R} i (x +_{C} y) j = algSc (P) (c))$
102	79 101	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x +_{C} y \in S$
103	102	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x +_{C} y \in S$

Metamath Proof Explorer

Theorem cpmatacl

Proof