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 ) )