Theorem mat1bas

Description: The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019)

	Ref	Expression
Hypotheses	mat1bas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat1bas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat1bas.i	⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
Assertion	mat1bas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mat1bas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mat1bas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		mat1bas.i	⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
4		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
5	4	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 Mat 𝑅 ) ∈ Ring )
6	5	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑁 Mat 𝑅 ) ∈ Ring )
7	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
8	2 7	eqtri	⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
9	8 3	ringidcl	⊢ ( ( 𝑁 Mat 𝑅 ) ∈ Ring → 1 ∈ 𝐵 )
10	6 9	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ 𝐵 )