# Metamath Proof Explorer

## Theorem mattposm

Description: Multiplying two transposed matrices results in the transposition of the product of the two matrices. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses mattposm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mattposm.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mattposm.t
Assertion mattposm

### Proof

Step Hyp Ref Expression
1 mattposm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mattposm.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 mattposm.t
4 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 simp1 ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {R}\in \mathrm{CRing}$
7 1 2 matrcl ${⊢}{Y}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
8 7 simpld ${⊢}{Y}\in {B}\to {N}\in \mathrm{Fin}$
9 8 3ad2ant3 ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {N}\in \mathrm{Fin}$
10 1 5 2 matbas2i ${⊢}{X}\in {B}\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
11 10 3ad2ant2 ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
12 1 5 2 matbas2i ${⊢}{Y}\in {B}\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
13 12 3ad2ant3 ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
14 4 4 5 6 9 9 9 11 13 mamutpos ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to tpos\left({X}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){Y}\right)=tpos{Y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)tpos{X}$
15 1 4 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
16 9 6 15 syl2anc ${⊢}\left({R}\in \mathrm{CRing}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
17 3 16 eqtr4id
18 17 oveqd
19 18 tposeqd
20 17 oveqd
21 14 19 20 3eqtr4d