# Metamath Proof Explorer

## Theorem eqmat

Description: Two square matrices of the same dimension are equal if they have the same entries. (Contributed by AV, 25-Sep-2019)

Ref Expression
Hypotheses eqmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
eqmat.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion eqmat ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}={Y}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{X}{j}={i}{Y}{j}\right)$

### Proof

Step Hyp Ref Expression
1 eqmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 eqmat.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
4 1 3 2 matbas2i ${⊢}{X}\in {B}\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
5 elmapfn ${⊢}{X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {X}Fn\left({N}×{N}\right)$
6 4 5 syl ${⊢}{X}\in {B}\to {X}Fn\left({N}×{N}\right)$
7 1 3 2 matbas2i ${⊢}{Y}\in {B}\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
8 elmapfn ${⊢}{Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {Y}Fn\left({N}×{N}\right)$
9 7 8 syl ${⊢}{Y}\in {B}\to {Y}Fn\left({N}×{N}\right)$
10 eqfnov2 ${⊢}\left({X}Fn\left({N}×{N}\right)\wedge {Y}Fn\left({N}×{N}\right)\right)\to \left({X}={Y}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{X}{j}={i}{Y}{j}\right)$
11 6 9 10 syl2an ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}={Y}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{X}{j}={i}{Y}{j}\right)$