Metamath Proof Explorer

Theorem mdetpmtr2

Description: The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses mdetpmtr.a 
|- A = ( N Mat R )
mdetpmtr.b 
|- B = ( Base ` A )
mdetpmtr.d 
|- D = ( N maDet R )
mdetpmtr.g 
|- G = ( Base ` ( SymGrp ` N ) )
mdetpmtr.s 
|- S = ( pmSgn ` N )
mdetpmtr.z 
|- Z = ( ZRHom ` R )
mdetpmtr.t 
|- .x. = ( .r ` R )
mdetpmtr2.e 
|- E = ( i e. N , j e. N |-> ( i M ( P ` j ) ) )
Assertion mdetpmtr2 
|- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )

Proof

Step Hyp Ref Expression
1 mdetpmtr.a 
 |-  A = ( N Mat R )
2 mdetpmtr.b 
 |-  B = ( Base ` A )
3 mdetpmtr.d 
 |-  D = ( N maDet R )
4 mdetpmtr.g 
 |-  G = ( Base ` ( SymGrp ` N ) )
5 mdetpmtr.s 
 |-  S = ( pmSgn ` N )
6 mdetpmtr.z 
 |-  Z = ( ZRHom ` R )
7 mdetpmtr.t 
 |-  .x. = ( .r ` R )
8 mdetpmtr2.e 
 |-  E = ( i e. N , j e. N |-> ( i M ( P ` j ) ) )
9 simpll 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> R e. CRing )
10 simplr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> N e. Fin )
11 1 2 mattposcl 
 |-  ( M e. B -> tpos M e. B )
12 11 ad2antrl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> tpos M e. B )
13 simprr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> P e. G )
14 ovtpos 
 |-  ( ( P ` j ) tpos M i ) = ( i M ( P ` j ) )
15 14 eqcomi 
 |-  ( i M ( P ` j ) ) = ( ( P ` j ) tpos M i )
16 15 a1i 
 |-  ( ( i e. N /\ j e. N ) -> ( i M ( P ` j ) ) = ( ( P ` j ) tpos M i ) )
17 16 mpoeq3ia 
 |-  ( i e. N , j e. N |-> ( i M ( P ` j ) ) ) = ( i e. N , j e. N |-> ( ( P ` j ) tpos M i ) )
18 8 17 eqtri 
 |-  E = ( i e. N , j e. N |-> ( ( P ` j ) tpos M i ) )
19 18 tposmpo 
 |-  tpos E = ( j e. N , i e. N |-> ( ( P ` j ) tpos M i ) )
20 1 2 3 4 5 6 7 19 mdetpmtr1 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( tpos M e. B /\ P e. G ) ) -> ( D ` tpos M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` tpos E ) ) )
21 9 10 12 13 20 syl22anc 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` tpos M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` tpos E ) ) )
22 3 1 2 mdettpos 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( D ` M ) )
23 22 ad2ant2r 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` tpos M ) = ( D ` M ) )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 simp2 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> i e. N )
26 13 3ad2ant1 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> P e. G )
27 simp3 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> j e. N )
28 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
29 28 4 symgfv 
 |-  ( ( P e. G /\ j e. N ) -> ( P ` j ) e. N )
30 26 27 29 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> ( P ` j ) e. N )
31 simp1rl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> M e. B )
32 1 24 2 25 30 31 matecld 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) /\ i e. N /\ j e. N ) -> ( i M ( P ` j ) ) e. ( Base ` R ) )
33 1 24 2 10 9 32 matbas2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( i e. N , j e. N |-> ( i M ( P ` j ) ) ) e. B )
34 8 33 eqeltrid 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> E e. B )
35 3 1 2 mdettpos 
 |-  ( ( R e. CRing /\ E e. B ) -> ( D ` tpos E ) = ( D ` E ) )
36 9 34 35 syl2anc 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` tpos E ) = ( D ` E ) )
37 36 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( ( ( Z o. S ) ` P ) .x. ( D ` tpos E ) ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )
38 21 23 37 3eqtr3d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )