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 Mat R )
	matmpo.n	|- B = ( Base ` A )
Assertion	matmpo	|- ( M e. B -> M = ( i e. N , j e. N |-> ( i M j ) ) )

Proof

Step	Hyp	Ref	Expression
1		matmpo.a	|- A = ( N Mat R )
2		matmpo.n	|- B = ( Base ` A )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4	1 3 2	matbas2i	|- ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
5		elmapfn	|- ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M Fn ( N X. N ) )
6	4 5	syl	|- ( M e. B -> M Fn ( N X. N ) )
7		fnov	|- ( M Fn ( N X. N ) <-> M = ( i e. N , j e. N |-> ( i M j ) ) )
8	6 7	sylib	|- ( M e. B -> M = ( i e. N , j e. N |-> ( i M j ) ) )