Theorem matmpo

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

	Ref	Expression
Hypotheses	matmpo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matmpo.n	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	matmpo	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) ) )

Proof

Step	Hyp	Ref	Expression
1		matmpo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matmpo.n	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	1 3 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
5		elmapfn	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 Fn ( 𝑁 × 𝑁 ) )
6	4 5	syl	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 Fn ( 𝑁 × 𝑁 ) )
7		fnov	⊢ ( 𝑀 Fn ( 𝑁 × 𝑁 ) ↔ 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) ) )
8	6 7	sylib	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) ) )