1elcpmat

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

	Ref	Expression
Hypotheses	cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
	cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
	cpmatsrngpmat.c	$⊢ C = N Mat P$
Assertion	1elcpmat	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \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}_{R} = {Base}_{R}$
5		eqid	$⊢ 1_{R} = 1_{R}$
6	4 5	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
7	6	ancli	$⊢ R \in Ring \to (R \in Ring \land 1_{R} \in {Base}_{R})$
8	7	adantl	$⊢ (N \in Fin \land R \in Ring) \to (R \in Ring \land 1_{R} \in {Base}_{R})$
9	8	ad2antrl	$⊢ (i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to (R \in Ring \land 1_{R} \in {Base}_{R})$
10		eqid	$⊢ 0_{R} = 0_{R}$
11		eqid	$⊢ {Base}_{P} = {Base}_{P}$
12		eqid	$⊢ algSc (P) = algSc (P)$
13	4 10 2 11 12	cply1coe0	$⊢ (R \in Ring \land 1_{R} \in {Base}_{R}) \to \forall n \in ℕ {coe}_{1} (algSc (P) (1_{R})) (n) = 0_{R}$
14	9 13	syl	$⊢ (i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to \forall n \in ℕ {coe}_{1} (algSc (P) (1_{R})) (n) = 0_{R}$
15		iftrue	$⊢ i = j \to if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R})) = algSc (P) (1_{R})$
16	15	fveq2d	$⊢ i = j \to {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) = {coe}_{1} (algSc (P) (1_{R}))$
17	16	fveq1d	$⊢ i = j \to {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = {coe}_{1} (algSc (P) (1_{R})) (n)$
18	17	eqeq1d	$⊢ i = j \to ({coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R} \leftrightarrow {coe}_{1} (algSc (P) (1_{R})) (n) = 0_{R})$
19	18	ralbidv	$⊢ i = j \to (\forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R} \leftrightarrow \forall n \in ℕ {coe}_{1} (algSc (P) (1_{R})) (n) = 0_{R})$
20	19	adantr	$⊢ (i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to (\forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R} \leftrightarrow \forall n \in ℕ {coe}_{1} (algSc (P) (1_{R})) (n) = 0_{R})$
21	14 20	mpbird	$⊢ (i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R}$
22	4 10	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
23	22	ancli	$⊢ R \in Ring \to (R \in Ring \land 0_{R} \in {Base}_{R})$
24	23	adantl	$⊢ (N \in Fin \land R \in Ring) \to (R \in Ring \land 0_{R} \in {Base}_{R})$
25	4 10 2 11 12	cply1coe0	$⊢ (R \in Ring \land 0_{R} \in {Base}_{R}) \to \forall n \in ℕ {coe}_{1} (algSc (P) (0_{R})) (n) = 0_{R}$
26	24 25	syl	$⊢ (N \in Fin \land R \in Ring) \to \forall n \in ℕ {coe}_{1} (algSc (P) (0_{R})) (n) = 0_{R}$
27	26	ad2antrl	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to \forall n \in ℕ {coe}_{1} (algSc (P) (0_{R})) (n) = 0_{R}$
28		iffalse	$⊢ \neg i = j \to if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R})) = algSc (P) (0_{R})$
29	28	adantr	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R})) = algSc (P) (0_{R})$
30	29	fveq2d	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) = {coe}_{1} (algSc (P) (0_{R}))$
31	30	fveq1d	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = {coe}_{1} (algSc (P) (0_{R})) (n)$
32	31	eqeq1d	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to ({coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R} \leftrightarrow {coe}_{1} (algSc (P) (0_{R})) (n) = 0_{R})$
33	32	ralbidv	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to (\forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R} \leftrightarrow \forall n \in ℕ {coe}_{1} (algSc (P) (0_{R})) (n) = 0_{R})$
34	27 33	mpbird	$⊢ (\neg i = j \land ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N))) \to \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R}$
35	21 34	pm2.61ian	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R}$
36	35	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R}$
37		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to N \in Fin$
38		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to R \in Ring$
39		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i \in N$
40		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to j \in N$
41		eqid	$⊢ 1_{C} = 1_{C}$
42	2 3 12 10 5 37 38 39 40 41	pmat1ovscd	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i 1_{C} j = if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))$
43	42	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to {coe}_{1} (i 1_{C} j) = {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R})))$
44	43	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to {coe}_{1} (i 1_{C} j) (n) = {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n)$
45	44	eqeq1d	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to ({coe}_{1} (i 1_{C} j) (n) = 0_{R} \leftrightarrow {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R})$
46	45	ralbidv	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to (\forall n \in ℕ {coe}_{1} (i 1_{C} j) (n) = 0_{R} \leftrightarrow \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R})$
47	46	2ralbidva	$⊢ (N \in Fin \land R \in Ring) \to (\forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i 1_{C} j) (n) = 0_{R} \leftrightarrow \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (if (i = j, algSc (P) (1_{R}), algSc (P) (0_{R}))) (n) = 0_{R})$
48	36 47	mpbird	$⊢ (N \in Fin \land R \in Ring) \to \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i 1_{C} j) (n) = 0_{R}$
49	2 3	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
50		eqid	$⊢ {Base}_{C} = {Base}_{C}$
51	50 41	ringidcl	$⊢ C \in Ring \to 1_{C} \in {Base}_{C}$
52	49 51	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in {Base}_{C}$
53	1 2 3 50	cpmatel	$⊢ (N \in Fin \land R \in Ring \land 1_{C} \in {Base}_{C}) \to (1_{C} \in S \leftrightarrow \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i 1_{C} j) (n) = 0_{R})$
54	52 53	mpd3an3	$⊢ (N \in Fin \land R \in Ring) \to (1_{C} \in S \leftrightarrow \forall i \in N \forall j \in N \forall n \in ℕ {coe}_{1} (i 1_{C} j) (n) = 0_{R})$
55	48 54	mpbird	$⊢ (N \in Fin \land R \in Ring) \to 1_{C} \in S$

Metamath Proof Explorer

Theorem 1elcpmat

Proof