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 Mat R
mattposm.b B = Base A
mattposm.t · ˙ = A
Assertion mattposm R CRing X B Y B tpos X · ˙ Y = tpos Y · ˙ tpos X

Proof

Step Hyp Ref Expression
1 mattposm.a A = N Mat R
2 mattposm.b B = Base A
3 mattposm.t · ˙ = A
4 eqid R maMul N N N = R maMul N N N
5 eqid Base R = Base R
6 simp1 R CRing X B Y B R CRing
7 1 2 matrcl Y B N Fin R V
8 7 simpld Y B N Fin
9 8 3ad2ant3 R CRing X B Y B N Fin
10 1 5 2 matbas2i X B X Base R N × N
11 10 3ad2ant2 R CRing X B Y B X Base R N × N
12 1 5 2 matbas2i Y B Y Base R N × N
13 12 3ad2ant3 R CRing X B Y B Y Base R N × N
14 4 4 5 6 9 9 9 11 13 mamutpos R CRing X B Y B tpos X R maMul N N N Y = tpos Y R maMul N N N tpos X
15 1 4 matmulr N Fin R CRing R maMul N N N = A
16 9 6 15 syl2anc R CRing X B Y B R maMul N N N = A
17 3 16 eqtr4id R CRing X B Y B · ˙ = R maMul N N N
18 17 oveqd R CRing X B Y B X · ˙ Y = X R maMul N N N Y
19 18 tposeqd R CRing X B Y B tpos X · ˙ Y = tpos X R maMul N N N Y
20 17 oveqd R CRing X B Y B tpos Y · ˙ tpos X = tpos Y R maMul N N N tpos X
21 14 19 20 3eqtr4d R CRing X B Y B tpos X · ˙ Y = tpos Y · ˙ tpos X