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 ⊢ A = N Mat R
eqmat.b ⊢ B = Base A
Assertion eqmat ⊢ X ∈ B ∧ Y ∈ B → X = Y ↔ ∀ i ∈ N ∀ j ∈ N i X j = i Y j

Proof

Step Hyp Ref Expression
1 eqmat.a ⊢ A = N Mat R
2 eqmat.b ⊢ B = Base A
3 eqid ⊢ Base R = Base R
4 1 3 2 matbas2i ⊢ X ∈ B → X ∈ Base R N × N
5 elmapfn ⊢ X ∈ Base R N × N → X Fn N × N
6 4 5 syl ⊢ X ∈ B → X Fn N × N
7 1 3 2 matbas2i ⊢ Y ∈ B → Y ∈ Base R N × N
8 elmapfn ⊢ Y ∈ Base R N × N → Y Fn N × N
9 7 8 syl ⊢ Y ∈ B → Y Fn N × N
10 eqfnov2 ⊢ X Fn N × N ∧ Y Fn N × N → X = Y ↔ ∀ i ∈ N ∀ j ∈ N i X j = i Y j
11 6 9 10 syl2an ⊢ X ∈ B ∧ Y ∈ B → X = Y ↔ ∀ i ∈ N ∀ j ∈ N i X j = i Y j