Metamath Proof Explorer

Theorem mdetpmtr12

Description: The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (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 )
mdetpmtr12.e 
|- E = ( i e. N , j e. N |-> ( ( P ` i ) M ( Q ` j ) ) )
mdetmptr12.r 
|- ( ph -> R e. CRing )
mdetmptr12.n 
|- ( ph -> N e. Fin )
mdetmptr12.m 
|- ( ph -> M e. B )
mdetmptr12.p 
|- ( ph -> P e. G )
mdetmptr12.q 
|- ( ph -> Q e. G )
Assertion mdetpmtr12 
|- ( ph -> ( D ` M ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .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 mdetpmtr12.e 
 |-  E = ( i e. N , j e. N |-> ( ( P ` i ) M ( Q ` j ) ) )
9 mdetmptr12.r 
 |-  ( ph -> R e. CRing )
10 mdetmptr12.n 
 |-  ( ph -> N e. Fin )
11 mdetmptr12.m 
 |-  ( ph -> M e. B )
12 mdetmptr12.p 
 |-  ( ph -> P e. G )
13 mdetmptr12.q 
 |-  ( ph -> Q e. G )
14 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
15 14 oveq1d 
 |-  ( k = i -> ( ( P ` k ) M l ) = ( ( P ` i ) M l ) )
16 oveq2 
 |-  ( l = j -> ( ( P ` i ) M l ) = ( ( P ` i ) M j ) )
17 15 16 cbvmpov 
 |-  ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) = ( i e. N , j e. N |-> ( ( P ` i ) M j ) )
18 1 2 3 4 5 6 7 17 mdetpmtr1 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) ) )
19 9 10 11 12 18 syl22anc 
 |-  ( ph -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) ) )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 12 3ad2ant1 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> P e. G )
22 simp2 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> k e. N )
23 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
24 23 4 symgfv 
 |-  ( ( P e. G /\ k e. N ) -> ( P ` k ) e. N )
25 21 22 24 syl2anc 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( P ` k ) e. N )
26 simp3 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> l e. N )
27 11 3ad2ant1 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> M e. B )
28 1 20 2 25 26 27 matecld 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( ( P ` k ) M l ) e. ( Base ` R ) )
29 1 20 2 10 9 28 matbas2d 
 |-  ( ph -> ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) e. B )
30 eqid 
 |-  ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) = ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) )
31 1 2 3 4 5 6 7 30 mdetpmtr2 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) e. B /\ Q e. G ) ) -> ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) = ( ( ( Z o. S ) ` Q ) .x. ( D ` ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) ) ) )
32 9 10 29 13 31 syl22anc 
 |-  ( ph -> ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) = ( ( ( Z o. S ) ` Q ) .x. ( D ` ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) ) ) )
33 simp2 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> i e. N )
34 13 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Q e. G )
35 simp3 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> j e. N )
36 23 4 symgfv 
 |-  ( ( Q e. G /\ j e. N ) -> ( Q ` j ) e. N )
37 34 35 36 syl2anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( Q ` j ) e. N )
38 oveq2 
 |-  ( l = ( Q ` j ) -> ( ( P ` i ) M l ) = ( ( P ` i ) M ( Q ` j ) ) )
39 eqid 
 |-  ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) = ( k e. N , l e. N |-> ( ( P ` k ) M l ) )
40 ovex 
 |-  ( ( P ` i ) M ( Q ` j ) ) e. _V
41 15 38 39 40 ovmpo 
 |-  ( ( i e. N /\ ( Q ` j ) e. N ) -> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) = ( ( P ` i ) M ( Q ` j ) ) )
42 33 37 41 syl2anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) = ( ( P ` i ) M ( Q ` j ) ) )
43 42 mpoeq3dva 
 |-  ( ph -> ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) = ( i e. N , j e. N |-> ( ( P ` i ) M ( Q ` j ) ) ) )
44 8 43 eqtr4id 
 |-  ( ph -> E = ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) )
45 44 fveq2d 
 |-  ( ph -> ( D ` E ) = ( D ` ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) ) )
46 45 oveq2d 
 |-  ( ph -> ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) = ( ( ( Z o. S ) ` Q ) .x. ( D ` ( i e. N , j e. N |-> ( i ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ( Q ` j ) ) ) ) ) )
47 32 46 eqtr4d 
 |-  ( ph -> ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) = ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) )
48 47 oveq2d 
 |-  ( ph -> ( ( ( Z o. S ) ` P ) .x. ( D ` ( k e. N , l e. N |-> ( ( P ` k ) M l ) ) ) ) = ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) ) )
49 crngring 
 |-  ( R e. CRing -> R e. Ring )
50 9 49 syl 
 |-  ( ph -> R e. Ring )
51 4 5 6 zrhcopsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ P e. G ) -> ( ( Z o. S ) ` P ) e. ( Base ` R ) )
52 50 10 12 51 syl3anc 
 |-  ( ph -> ( ( Z o. S ) ` P ) e. ( Base ` R ) )
53 4 5 6 zrhcopsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. G ) -> ( ( Z o. S ) ` Q ) e. ( Base ` R ) )
54 50 10 13 53 syl3anc 
 |-  ( ph -> ( ( Z o. S ) ` Q ) e. ( Base ` R ) )
55 12 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> P e. G )
56 23 4 symgfv 
 |-  ( ( P e. G /\ i e. N ) -> ( P ` i ) e. N )
57 55 33 56 syl2anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( P ` i ) e. N )
58 11 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> M e. B )
59 1 20 2 57 37 58 matecld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( ( P ` i ) M ( Q ` j ) ) e. ( Base ` R ) )
60 1 20 2 10 9 59 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> ( ( P ` i ) M ( Q ` j ) ) ) e. B )
61 8 60 eqeltrid 
 |-  ( ph -> E e. B )
62 3 1 2 20 mdetcl 
 |-  ( ( R e. CRing /\ E e. B ) -> ( D ` E ) e. ( Base ` R ) )
63 9 61 62 syl2anc 
 |-  ( ph -> ( D ` E ) e. ( Base ` R ) )
64 20 7 ringass 
 |-  ( ( R e. Ring /\ ( ( ( Z o. S ) ` P ) e. ( Base ` R ) /\ ( ( Z o. S ) ` Q ) e. ( Base ` R ) /\ ( D ` E ) e. ( Base ` R ) ) ) -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` Q ) ) .x. ( D ` E ) ) = ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) ) )
65 50 52 54 63 64 syl13anc 
 |-  ( ph -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` Q ) ) .x. ( D ` E ) ) = ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) ) )
66 4 5 cofipsgn 
 |-  ( ( N e. Fin /\ P e. G ) -> ( ( Z o. S ) ` P ) = ( Z ` ( S ` P ) ) )
67 10 12 66 syl2anc 
 |-  ( ph -> ( ( Z o. S ) ` P ) = ( Z ` ( S ` P ) ) )
68 4 5 cofipsgn 
 |-  ( ( N e. Fin /\ Q e. G ) -> ( ( Z o. S ) ` Q ) = ( Z ` ( S ` Q ) ) )
69 10 13 68 syl2anc 
 |-  ( ph -> ( ( Z o. S ) ` Q ) = ( Z ` ( S ` Q ) ) )
70 67 69 oveq12d 
 |-  ( ph -> ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` Q ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` Q ) ) ) )
71 6 zrhrhm 
 |-  ( R e. Ring -> Z e. ( ZZring RingHom R ) )
72 50 71 syl 
 |-  ( ph -> Z e. ( ZZring RingHom R ) )
73 1z 
 |-  1 e. ZZ
74 neg1z 
 |-  -u 1 e. ZZ
75 prssi 
 |-  ( ( 1 e. ZZ /\ -u 1 e. ZZ ) -> { 1 , -u 1 } C_ ZZ )
76 73 74 75 mp2an 
 |-  { 1 , -u 1 } C_ ZZ
77 4 5 psgnran 
 |-  ( ( N e. Fin /\ P e. G ) -> ( S ` P ) e. { 1 , -u 1 } )
78 10 12 77 syl2anc 
 |-  ( ph -> ( S ` P ) e. { 1 , -u 1 } )
79 76 78 sselid 
 |-  ( ph -> ( S ` P ) e. ZZ )
80 4 5 psgnran 
 |-  ( ( N e. Fin /\ Q e. G ) -> ( S ` Q ) e. { 1 , -u 1 } )
81 10 13 80 syl2anc 
 |-  ( ph -> ( S ` Q ) e. { 1 , -u 1 } )
82 76 81 sselid 
 |-  ( ph -> ( S ` Q ) e. ZZ )
83 zringbas 
 |-  ZZ = ( Base ` ZZring )
84 zringmulr 
 |-  x. = ( .r ` ZZring )
85 83 84 7 rhmmul 
 |-  ( ( Z e. ( ZZring RingHom R ) /\ ( S ` P ) e. ZZ /\ ( S ` Q ) e. ZZ ) -> ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` Q ) ) ) )
86 72 79 82 85 syl3anc 
 |-  ( ph -> ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) = ( ( Z ` ( S ` P ) ) .x. ( Z ` ( S ` Q ) ) ) )
87 70 86 eqtr4d 
 |-  ( ph -> ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` Q ) ) = ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) )
88 87 oveq1d 
 |-  ( ph -> ( ( ( ( Z o. S ) ` P ) .x. ( ( Z o. S ) ` Q ) ) .x. ( D ` E ) ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` E ) ) )
89 65 88 eqtr3d 
 |-  ( ph -> ( ( ( Z o. S ) ` P ) .x. ( ( ( Z o. S ) ` Q ) .x. ( D ` E ) ) ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` E ) ) )
90 19 48 89 3eqtrd 
 |-  ( ph -> ( D ` M ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` E ) ) )