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 e. B /\ Y e. B ) -> ( X = Y <-> A. i e. N A. j e. 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 e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
5 elmapfn 
 |-  ( X e. ( ( Base ` R ) ^m ( N X. N ) ) -> X Fn ( N X. N ) )
6 4 5 syl 
 |-  ( X e. B -> X Fn ( N X. N ) )
7 1 3 2 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
8 elmapfn 
 |-  ( Y e. ( ( Base ` R ) ^m ( N X. N ) ) -> Y Fn ( N X. N ) )
9 7 8 syl 
 |-  ( Y e. B -> Y Fn ( N X. N ) )
10 eqfnov2 
 |-  ( ( X Fn ( N X. N ) /\ Y Fn ( N X. N ) ) -> ( X = Y <-> A. i e. N A. j e. N ( i X j ) = ( i Y j ) ) )
11 6 9 10 syl2an 
 |-  ( ( X e. B /\ Y e. B ) -> ( X = Y <-> A. i e. N A. j e. N ( i X j ) = ( i Y j ) ) )