# 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}\mathrm{Mat}{R}$
mattposvs.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mattposvs.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
mattposvs.v
Assertion mattposvs

### Proof

Step Hyp Ref Expression
1 mattposvs.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mattposvs.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 mattposvs.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
4 mattposvs.v
5 1 2 matrcl ${⊢}{Y}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
6 5 simpld ${⊢}{Y}\in {B}\to {N}\in \mathrm{Fin}$
7 sqxpexg ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{V}$
8 6 7 syl ${⊢}{Y}\in {B}\to {N}×{N}\in \mathrm{V}$
9 snex ${⊢}\left\{{X}\right\}\in \mathrm{V}$
10 xpexg ${⊢}\left({N}×{N}\in \mathrm{V}\wedge \left\{{X}\right\}\in \mathrm{V}\right)\to \left({N}×{N}\right)×\left\{{X}\right\}\in \mathrm{V}$
11 8 9 10 sylancl ${⊢}{Y}\in {B}\to \left({N}×{N}\right)×\left\{{X}\right\}\in \mathrm{V}$
12 oftpos ${⊢}\left(\left({N}×{N}\right)×\left\{{X}\right\}\in \mathrm{V}\wedge {Y}\in {B}\right)\to tpos\left(\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}{Y}\right)=tpos\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}$
13 11 12 mpancom ${⊢}{Y}\in {B}\to tpos\left(\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}{Y}\right)=tpos\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}$
14 tposconst ${⊢}tpos\left(\left({N}×{N}\right)×\left\{{X}\right\}\right)=\left({N}×{N}\right)×\left\{{X}\right\}$
15 14 oveq1i ${⊢}tpos\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}=\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}$
16 13 15 eqtrdi ${⊢}{Y}\in {B}\to tpos\left(\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}{Y}\right)=\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}$
17 16 adantl ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to tpos\left(\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}{Y}\right)=\left(\left({N}×{N}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}tpos{Y}$
18 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
19 eqid ${⊢}{N}×{N}={N}×{N}$
20 1 2 3 4 18 19 matvsca2
21 20 tposeqd
22 1 2 mattposcl ${⊢}{Y}\in {B}\to tpos{Y}\in {B}$
23 1 2 3 4 18 19 matvsca2
24 22 23 sylan2
25 17 21 24 3eqtr4d