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 
|- .x. = ( .r ` A )
Assertion mattposm 
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X .x. Y ) = ( tpos Y .x. tpos X ) )

Proof

Step Hyp Ref Expression
1 mattposm.a 
 |-  A = ( N Mat R )
2 mattposm.b 
 |-  B = ( Base ` A )
3 mattposm.t 
 |-  .x. = ( .r ` A )
4 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 simp1 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> R e. CRing )
7 1 2 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
8 7 simpld 
 |-  ( Y e. B -> N e. Fin )
9 8 3ad2ant3 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> N e. Fin )
10 1 5 2 matbas2i 
 |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
11 10 3ad2ant2 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
12 1 5 2 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
13 12 3ad2ant3 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
14 4 4 5 6 9 9 9 11 13 mamutpos 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X ( R maMul <. N , N , N >. ) Y ) = ( tpos Y ( R maMul <. N , N , N >. ) tpos X ) )
15 1 4 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
16 9 6 15 syl2anc 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
17 3 16 eqtr4id 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> .x. = ( R maMul <. N , N , N >. ) )
18 17 oveqd 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X ( R maMul <. N , N , N >. ) Y ) )
19 18 tposeqd 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X .x. Y ) = tpos ( X ( R maMul <. N , N , N >. ) Y ) )
20 17 oveqd 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( tpos Y .x. tpos X ) = ( tpos Y ( R maMul <. N , N , N >. ) tpos X ) )
21 14 19 20 3eqtr4d 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X .x. Y ) = ( tpos Y .x. tpos X ) )