cpmatmcl

Description: The set of all constant polynomial matrices over a ring R is closed under multiplication. (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	cpmatmcl	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x \cdot_{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	1 2 3	cpmatmcllem	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}$
5	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
6	5	ad4antlr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to P \in Ring$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8	1 2 3 7	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to x \in {Base}_{C}$
9	8	3expa	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to x \in {Base}_{C}$
10	1 2 3 7	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land y \in S) \to y \in {Base}_{C}$
11	10	3expa	$⊢ ((N \in Fin \land R \in Ring) \land y \in S) \to y \in {Base}_{C}$
12	9 11	anim12dan	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (x \in {Base}_{C} \land y \in {Base}_{C})$
13	12	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \to (x \in {Base}_{C} \land y \in {Base}_{C})$
14	13	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to (x \in {Base}_{C} \land y \in {Base}_{C})$
15		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \to i \in N$
16	15	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to (i \in N \land j \in N)$
17		eqid	$⊢ \cdot_{C} = \cdot_{C}$
18	3 7 17	matmulcell	$⊢ (P \in Ring \land (x \in {Base}_{C} \land y \in {Base}_{C}) \land (i \in N \land j \in N)) \to i (x \cdot_{C} y) j = \underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))$
19	6 14 16 18	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to i (x \cdot_{C} y) j = \underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))$
20	19	fveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) = {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j)))$
21	20	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \land c \in ℕ) \to {coe}_{1} (i (x \cdot_{C} y) j) = {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j)))$
22	21	fveq1d	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \land c \in ℕ) \to {coe}_{1} (i (x \cdot_{C} y) j) (c) = {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c)$
23	22	eqeq1d	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \land c \in ℕ) \to ({coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R} \leftrightarrow {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
24	23	ralbidva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \land j \in N) \to (\forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R} \leftrightarrow \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
25	24	ralbidva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \land i \in N) \to (\forall j \in N \forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R} \leftrightarrow \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
26	25	ralbidva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (\forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R} \leftrightarrow \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
27	4 26	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R}$
28		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
29	28	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to N \in Fin$
30		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
31	30	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to R \in Ring$
32	2 3	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
33	32	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to C \in Ring$
34		simpl	$⊢ (x \in S \land y \in S) \to x \in S$
35	34	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)$
36		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)$
37	35 36	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)$
38	37 8	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \in {Base}_{C}$
39		simpr	$⊢ (x \in S \land y \in S) \to y \in S$
40	39	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)$
41		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)$
42	40 41	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)$
43	42 10	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to y \in {Base}_{C}$
44	7 17	ringcl	$⊢ (C \in Ring \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x \cdot_{C} y \in {Base}_{C}$
45	33 38 43 44	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \cdot_{C} y \in {Base}_{C}$
46	1 2 3 7	cpmatel	$⊢ (N \in Fin \land R \in Ring \land x \cdot_{C} y \in {Base}_{C}) \to (x \cdot_{C} y \in S \leftrightarrow \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R})$
47	29 31 45 46	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to (x \cdot_{C} y \in S \leftrightarrow \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (i (x \cdot_{C} y) j) (c) = 0_{R})$
48	27 47	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to x \cdot_{C} y \in S$
49	48	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S \forall y \in S x \cdot_{C} y \in S$

Metamath Proof Explorer

Theorem cpmatmcl

Proof