Metamath Proof Explorer

Theorem mattposcl

Description: The transpose of a square matrix is a square matrix of the same size. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses mattposcl.a 
|- A = ( N Mat R )
mattposcl.b 
|- B = ( Base ` A )
Assertion mattposcl 
|- ( M e. B -> tpos M e. B )

Proof

Step Hyp Ref Expression
1 mattposcl.a 
 |-  A = ( N Mat R )
2 mattposcl.b 
 |-  B = ( Base ` A )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 1 3 2 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
5 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
6 tposf 
 |-  ( M : ( N X. N ) --> ( Base ` R ) -> tpos M : ( N X. N ) --> ( Base ` R ) )
7 4 5 6 3syl 
 |-  ( M e. B -> tpos M : ( N X. N ) --> ( Base ` R ) )
8 fvex 
 |-  ( Base ` R ) e. _V
9 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
10 9 simpld 
 |-  ( M e. B -> N e. Fin )
11 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
12 11 anidms 
 |-  ( N e. Fin -> ( N X. N ) e. Fin )
13 10 12 syl 
 |-  ( M e. B -> ( N X. N ) e. Fin )
14 elmapg 
 |-  ( ( ( Base ` R ) e. _V /\ ( N X. N ) e. Fin ) -> ( tpos M e. ( ( Base ` R ) ^m ( N X. N ) ) <-> tpos M : ( N X. N ) --> ( Base ` R ) ) )
15 8 13 14 sylancr 
 |-  ( M e. B -> ( tpos M e. ( ( Base ` R ) ^m ( N X. N ) ) <-> tpos M : ( N X. N ) --> ( Base ` R ) ) )
16 7 15 mpbird 
 |-  ( M e. B -> tpos M e. ( ( Base ` R ) ^m ( N X. N ) ) )
17 1 3 matbas2 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
18 9 17 syl 
 |-  ( M e. B -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
19 18 2 eqtr4di 
 |-  ( M e. B -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
20 16 19 eleqtrd 
 |-  ( M e. B -> tpos M e. B )