Metamath Proof Explorer


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𝐵 )