Metamath Proof Explorer

Theorem mdettpos

Description: Determinant is invariant under transposition. Proposition 4.8 in Lang p. 514. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Hypotheses mdettpos.d 
|- D = ( N maDet R )
mdettpos.a 
|- A = ( N Mat R )
mdettpos.b 
|- B = ( Base ` A )
Assertion mdettpos 
|- ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( D ` M ) )

Proof

Step Hyp Ref Expression
1 mdettpos.d 
 |-  D = ( N maDet R )
2 mdettpos.a 
 |-  A = ( N Mat R )
3 mdettpos.b 
 |-  B = ( Base ` A )
4 ovtpos 
 |-  ( ( p ` x ) tpos M x ) = ( x M ( p ` x ) )
5 4 mpteq2i 
 |-  ( x e. N |-> ( ( p ` x ) tpos M x ) ) = ( x e. N |-> ( x M ( p ` x ) ) )
6 5 oveq2i 
 |-  ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. N |-> ( x M ( p ` x ) ) ) )
7 6 oveq2i 
 |-  ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) )
8 7 mpteq2i 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) )
9 8 oveq2i 
 |-  ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) )
10 2 3 mattposcl 
 |-  ( M e. B -> tpos M e. B )
11 10 adantl 
 |-  ( ( R e. CRing /\ M e. B ) -> tpos M e. B )
12 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
13 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
14 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
17 1 2 3 12 13 14 15 16 mdetleib 
 |-  ( tpos M e. B -> ( D ` tpos M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) ) ) ) )
18 11 17 syl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) tpos M x ) ) ) ) ) ) )
19 1 2 3 12 13 14 15 16 mdetleib2 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( x M ( p ` x ) ) ) ) ) ) ) )
20 9 18 19 3eqtr4a 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( D ` M ) )