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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	eqmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	eqmat	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑋 𝑗 ) = ( 𝑖 𝑌 𝑗 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		eqmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	1 3 2	matbas2i	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
5		elmapfn	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 Fn ( 𝑁 × 𝑁 ) )
6	4 5	syl	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 Fn ( 𝑁 × 𝑁 ) )
7	1 3 2	matbas2i	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
8		elmapfn	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑌 Fn ( 𝑁 × 𝑁 ) )
9	7 8	syl	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 Fn ( 𝑁 × 𝑁 ) )
10		eqfnov2	⊢ ( ( 𝑋 Fn ( 𝑁 × 𝑁 ) ∧ 𝑌 Fn ( 𝑁 × 𝑁 ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑋 𝑗 ) = ( 𝑖 𝑌 𝑗 ) ) )
11	6 9 10	syl2an	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑋 𝑗 ) = ( 𝑖 𝑌 𝑗 ) ) )