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=NMatR
mattposm.b B=BaseA
mattposm.t ·˙=A
Assertion mattposm RCRingXBYBtposX·˙Y=tposY·˙tposX

Proof

Step Hyp Ref Expression
1 mattposm.a A=NMatR
2 mattposm.b B=BaseA
3 mattposm.t ·˙=A
4 eqid RmaMulNNN=RmaMulNNN
5 eqid BaseR=BaseR
6 simp1 RCRingXBYBRCRing
7 1 2 matrcl YBNFinRV
8 7 simpld YBNFin
9 8 3ad2ant3 RCRingXBYBNFin
10 1 5 2 matbas2i XBXBaseRN×N
11 10 3ad2ant2 RCRingXBYBXBaseRN×N
12 1 5 2 matbas2i YBYBaseRN×N
13 12 3ad2ant3 RCRingXBYBYBaseRN×N
14 4 4 5 6 9 9 9 11 13 mamutpos RCRingXBYBtposXRmaMulNNNY=tposYRmaMulNNNtposX
15 1 4 matmulr NFinRCRingRmaMulNNN=A
16 9 6 15 syl2anc RCRingXBYBRmaMulNNN=A
17 3 16 eqtr4id RCRingXBYB·˙=RmaMulNNN
18 17 oveqd RCRingXBYBX·˙Y=XRmaMulNNNY
19 18 tposeqd RCRingXBYBtposX·˙Y=tposXRmaMulNNNY
20 17 oveqd RCRingXBYBtposY·˙tposX=tposYRmaMulNNNtposX
21 14 19 20 3eqtr4d RCRingXBYBtposX·˙Y=tposY·˙tposX