Metamath Proof Explorer

Theorem mamutpos

Description: Behavior of transposes in matrix products, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Hypotheses mamutpos.f 
|- F = ( R maMul <. M , N , P >. )
mamutpos.g 
|- G = ( R maMul <. P , N , M >. )
mamutpos.b 
|- B = ( Base ` R )
mamutpos.r 
|- ( ph -> R e. CRing )
mamutpos.m 
|- ( ph -> M e. Fin )
mamutpos.n 
|- ( ph -> N e. Fin )
mamutpos.p 
|- ( ph -> P e. Fin )
mamutpos.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamutpos.y 
|- ( ph -> Y e. ( B ^m ( N X. P ) ) )
Assertion mamutpos 
|- ( ph -> tpos ( X F Y ) = ( tpos Y G tpos X ) )

Proof

Step Hyp Ref Expression
1 mamutpos.f 
 |-  F = ( R maMul <. M , N , P >. )
2 mamutpos.g 
 |-  G = ( R maMul <. P , N , M >. )
3 mamutpos.b 
 |-  B = ( Base ` R )
4 mamutpos.r 
 |-  ( ph -> R e. CRing )
5 mamutpos.m 
 |-  ( ph -> M e. Fin )
6 mamutpos.n 
 |-  ( ph -> N e. Fin )
7 mamutpos.p 
 |-  ( ph -> P e. Fin )
8 mamutpos.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
9 mamutpos.y 
 |-  ( ph -> Y e. ( B ^m ( N X. P ) ) )
10 eqid 
 |-  ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) = ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) )
11 10 tposmpo 
 |-  tpos ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) = ( i e. P , j e. M |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) )
12 simpl1 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> ph )
13 12 4 syl 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> R e. CRing )
14 elmapi 
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
15 12 8 14 3syl 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> X : ( M X. N ) --> B )
16 simpl3 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> j e. M )
17 simpr 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> k e. N )
18 15 16 17 fovrnd 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> ( j X k ) e. B )
19 elmapi 
 |-  ( Y e. ( B ^m ( N X. P ) ) -> Y : ( N X. P ) --> B )
20 12 9 19 3syl 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> Y : ( N X. P ) --> B )
21 simpl2 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> i e. P )
22 20 17 21 fovrnd 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> ( k Y i ) e. B )
23 eqid 
 |-  ( .r ` R ) = ( .r ` R )
24 3 23 crngcom 
 |-  ( ( R e. CRing /\ ( j X k ) e. B /\ ( k Y i ) e. B ) -> ( ( j X k ) ( .r ` R ) ( k Y i ) ) = ( ( k Y i ) ( .r ` R ) ( j X k ) ) )
25 13 18 22 24 syl3anc 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> ( ( j X k ) ( .r ` R ) ( k Y i ) ) = ( ( k Y i ) ( .r ` R ) ( j X k ) ) )
26 ovtpos 
 |-  ( i tpos Y k ) = ( k Y i )
27 ovtpos 
 |-  ( k tpos X j ) = ( j X k )
28 26 27 oveq12i 
 |-  ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) = ( ( k Y i ) ( .r ` R ) ( j X k ) )
29 25 28 eqtr4di 
 |-  ( ( ( ph /\ i e. P /\ j e. M ) /\ k e. N ) -> ( ( j X k ) ( .r ` R ) ( k Y i ) ) = ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) )
30 29 mpteq2dva 
 |-  ( ( ph /\ i e. P /\ j e. M ) -> ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) = ( k e. N |-> ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) ) )
31 30 oveq2d 
 |-  ( ( ph /\ i e. P /\ j e. M ) -> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) = ( R gsum ( k e. N |-> ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) ) ) )
32 31 mpoeq3dva 
 |-  ( ph -> ( i e. P , j e. M |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) = ( i e. P , j e. M |-> ( R gsum ( k e. N |-> ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) ) ) ) )
33 11 32 syl5eq 
 |-  ( ph -> tpos ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) = ( i e. P , j e. M |-> ( R gsum ( k e. N |-> ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) ) ) ) )
34 1 3 23 4 5 6 7 8 9 mamuval 
 |-  ( ph -> ( X F Y ) = ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) )
35 34 tposeqd 
 |-  ( ph -> tpos ( X F Y ) = tpos ( j e. M , i e. P |-> ( R gsum ( k e. N |-> ( ( j X k ) ( .r ` R ) ( k Y i ) ) ) ) ) )
36 tposmap 
 |-  ( Y e. ( B ^m ( N X. P ) ) -> tpos Y e. ( B ^m ( P X. N ) ) )
37 9 36 syl 
 |-  ( ph -> tpos Y e. ( B ^m ( P X. N ) ) )
38 tposmap 
 |-  ( X e. ( B ^m ( M X. N ) ) -> tpos X e. ( B ^m ( N X. M ) ) )
39 8 38 syl 
 |-  ( ph -> tpos X e. ( B ^m ( N X. M ) ) )
40 2 3 23 4 7 6 5 37 39 mamuval 
 |-  ( ph -> ( tpos Y G tpos X ) = ( i e. P , j e. M |-> ( R gsum ( k e. N |-> ( ( i tpos Y k ) ( .r ` R ) ( k tpos X j ) ) ) ) ) )
41 33 35 40 3eqtr4d 
 |-  ( ph -> tpos ( X F Y ) = ( tpos Y G tpos X ) )