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