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	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmatsrngpmat.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	cpmatsrngpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion	1elcpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1_r ‘ 𝐶 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		cpmatsrngpmat.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		cpmatsrngpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
6	4 5	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
7	6	ancli	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
8	7	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
9	8	ad2antrl	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
10		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
11		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
12		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13	4 10 2 11 12	cply1coe0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
14	9 13	syl	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
15		iftrue	⊢ ( 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) )
16	15	fveq2d	⊢ ( 𝑖 = 𝑗 → ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) = ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) )
17	16	fveq1d	⊢ ( 𝑖 = 𝑗 → ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) )
18	17	eqeq1d	⊢ ( 𝑖 = 𝑗 → ( ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
19	18	ralbidv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
20	19	adantr	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
21	14 20	mpbird	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
22	4 10	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
23	22	ancli	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ Ring ∧ ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
24	23	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Ring ∧ ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
25	4 10 2 11 12	cply1coe0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
26	24 25	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
27	26	ad2antrl	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
28		iffalse	⊢ ( ¬ 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) )
29	28	adantr	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) )
30	29	fveq2d	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) = ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) )
31	30	fveq1d	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) )
32	31	eqeq1d	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
33	32	ralbidv	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
34	27 33	mpbird	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
35	21 34	pm2.61ian	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
36	35	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
37		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
38		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
39		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
40		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
41		eqid	⊢ ( 1_r ‘ 𝐶 ) = ( 1_r ‘ 𝐶 )
42	2 3 12 10 5 37 38 39 40 41	pmat1ovscd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) )
43	42	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) = ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) )
44	43	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) )
45	44	eqeq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
46	45	ralbidv	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
47	46	2ralbidva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0_g ‘ 𝑅 ) ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
48	36 47	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
49	2 3	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
50		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
51	50 41	ringidcl	⊢ ( 𝐶 ∈ Ring → ( 1_r ‘ 𝐶 ) ∈ ( Base ‘ 𝐶 ) )
52	49 51	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1_r ‘ 𝐶 ) ∈ ( Base ‘ 𝐶 ) )
53	1 2 3 50	cpmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝐶 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( 1_r ‘ 𝐶 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
54	52 53	mpd3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1_r ‘ 𝐶 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 ( 1_r ‘ 𝐶 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
55	48 54	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1_r ‘ 𝐶 ) ∈ 𝑆 )

Metamath Proof Explorer

Theorem 1elcpmat

Proof