This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑋 𝑗 ) = ( 𝑖 𝑌 𝑗 ) ) )