Metamath Proof Explorer

Theorem mattposvs

Description: The transposition of a matrix multiplied with a scalar equals the transposed matrix multiplied with the scalar, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses mattposvs.a 
|- A = ( N Mat R )
mattposvs.b 
|- B = ( Base ` A )
mattposvs.k 
|- K = ( Base ` R )
mattposvs.v 
|- .x. = ( .s ` A )
Assertion mattposvs 
|- ( ( X e. K /\ Y e. B ) -> tpos ( X .x. Y ) = ( X .x. tpos Y ) )

Proof

Step Hyp Ref Expression
1 mattposvs.a 
 |-  A = ( N Mat R )
2 mattposvs.b 
 |-  B = ( Base ` A )
3 mattposvs.k 
 |-  K = ( Base ` R )
4 mattposvs.v 
 |-  .x. = ( .s ` A )
5 1 2 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
6 5 simpld 
 |-  ( Y e. B -> N e. Fin )
7 sqxpexg 
 |-  ( N e. Fin -> ( N X. N ) e. _V )
8 6 7 syl 
 |-  ( Y e. B -> ( N X. N ) e. _V )
9 snex 
 |-  { X } e. _V
10 xpexg 
 |-  ( ( ( N X. N ) e. _V /\ { X } e. _V ) -> ( ( N X. N ) X. { X } ) e. _V )
11 8 9 10 sylancl 
 |-  ( Y e. B -> ( ( N X. N ) X. { X } ) e. _V )
12 oftpos 
 |-  ( ( ( ( N X. N ) X. { X } ) e. _V /\ Y e. B ) -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
13 11 12 mpancom 
 |-  ( Y e. B -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
14 tposconst 
 |-  tpos ( ( N X. N ) X. { X } ) = ( ( N X. N ) X. { X } )
15 14 oveq1i 
 |-  ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y )
16 13 15 eqtrdi 
 |-  ( Y e. B -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
17 16 adantl 
 |-  ( ( X e. K /\ Y e. B ) -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 eqid 
 |-  ( N X. N ) = ( N X. N )
20 1 2 3 4 18 19 matvsca2 
 |-  ( ( X e. K /\ Y e. B ) -> ( X .x. Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) )
21 20 tposeqd 
 |-  ( ( X e. K /\ Y e. B ) -> tpos ( X .x. Y ) = tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) )
22 1 2 mattposcl 
 |-  ( Y e. B -> tpos Y e. B )
23 1 2 3 4 18 19 matvsca2 
 |-  ( ( X e. K /\ tpos Y e. B ) -> ( X .x. tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
24 22 23 sylan2 
 |-  ( ( X e. K /\ Y e. B ) -> ( X .x. tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) )
25 17 21 24 3eqtr4d 
 |-  ( ( X e. K /\ Y e. B ) -> tpos ( X .x. Y ) = ( X .x. tpos Y ) )