Theorem matmpo

Description: Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020)

	Ref	Expression
Hypotheses	matmpo.a	$$⊢A=N\mathrm{Mat}R$$
	matmpo.n	$$⊢B={\mathrm{Base}}_A$$
Assertion	matmpo	$$⊢M\in B\to M=\left(i\in N,j\in N⟼iMj\right)$$

Proof

Step	Hyp	Ref	Expression
1		matmpo.a	$$⊢A=N\mathrm{Mat}R$$
2		matmpo.n	$$⊢B={\mathrm{Base}}_A$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	1 3 2	matbas2i	$$⊢M\in B\to M\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)$$
5		elmapfn	$$⊢M\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\to MFn\left(N\times N\right)$$
6	4 5	syl	$$⊢M\in B\to MFn\left(N\times N\right)$$
7		fnov	$$⊢MFn\left(N\times N\right)\leftrightarrow M=\left(i\in N,j\in N⟼iMj\right)$$
8	6 7	sylib	$$⊢M\in B\to M=\left(i\in N,j\in N⟼iMj\right)$$