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\leftrightarrow \forall i\in N\forall j\in NiXj=iYj\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\times N\right)}\right)$$
5		elmapfn	$$⊢X\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\to XFn\left(N\times N\right)$$
6	4 5	syl	$$⊢X\in B\to XFn\left(N\times N\right)$$
7	1 3 2	matbas2i	$$⊢Y\in B\to Y\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)$$
8		elmapfn	$$⊢Y\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\to YFn\left(N\times N\right)$$
9	7 8	syl	$$⊢Y\in B\to YFn\left(N\times N\right)$$
10		eqfnov2	$$⊢\left(XFn\left(N\times N\right)\wedge YFn\left(N\times N\right)\right)\to \left(X=Y\leftrightarrow \forall i\in N\forall j\in NiXj=iYj\right)$$
11	6 9 10	syl2an	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X=Y\leftrightarrow \forall i\in N\forall j\in NiXj=iYj\right)$$