MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetralt Structured version   Unicode version

Theorem mdetralt 18980
Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 23-Jul-2018.)
Hypotheses
Ref Expression
mdetralt.d  |-  D  =  ( N maDet  R )
mdetralt.a  |-  A  =  ( N Mat  R )
mdetralt.b  |-  B  =  ( Base `  A
)
mdetralt.z  |-  .0.  =  ( 0g `  R )
mdetralt.r  |-  ( ph  ->  R  e.  CRing )
mdetralt.x  |-  ( ph  ->  X  e.  B )
mdetralt.i  |-  ( ph  ->  I  e.  N )
mdetralt.j  |-  ( ph  ->  J  e.  N )
mdetralt.ij  |-  ( ph  ->  I  =/=  J )
mdetralt.eq  |-  ( ph  ->  A. a  e.  N  ( I X a )  =  ( J X a ) )
Assertion
Ref Expression
mdetralt  |-  ( ph  ->  ( D `  X
)  =  .0.  )
Distinct variable groups:    I, a    J, a    N, a    X, a
Allowed substitution hints:    ph( a)    A( a)    B( a)    D( a)    R( a)    .0. ( a)

Proof of Theorem mdetralt
Dummy variables  c  p  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetralt.x . . 3  |-  ( ph  ->  X  e.  B )
2 mdetralt.d . . . 4  |-  D  =  ( N maDet  R )
3 mdetralt.a . . . 4  |-  A  =  ( N Mat  R )
4 mdetralt.b . . . 4  |-  B  =  ( Base `  A
)
5 eqid 2441 . . . 4  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
6 eqid 2441 . . . 4  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
7 eqid 2441 . . . 4  |-  (pmSgn `  N )  =  (pmSgn `  N )
8 eqid 2441 . . . 4  |-  ( .r
`  R )  =  ( .r `  R
)
9 eqid 2441 . . . 4  |-  (mulGrp `  R )  =  (mulGrp `  R )
102, 3, 4, 5, 6, 7, 8, 9mdetleib 18959 . . 3  |-  ( X  e.  B  ->  ( D `  X )  =  ( R  gsumg  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )
111, 10syl 16 . 2  |-  ( ph  ->  ( D `  X
)  =  ( R 
gsumg  ( p  e.  ( Base `  ( SymGrp `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) ) ) )
12 eqid 2441 . . 3  |-  ( Base `  R )  =  (
Base `  R )
13 eqid 2441 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
14 mdetralt.r . . . . 5  |-  ( ph  ->  R  e.  CRing )
15 crngring 17080 . . . . 5  |-  ( R  e.  CRing  ->  R  e.  Ring )
1614, 15syl 16 . . . 4  |-  ( ph  ->  R  e.  Ring )
17 ringcmn 17100 . . . 4  |-  ( R  e.  Ring  ->  R  e. CMnd
)
1816, 17syl 16 . . 3  |-  ( ph  ->  R  e. CMnd )
193, 4matrcl 18784 . . . . . 6  |-  ( X  e.  B  ->  ( N  e.  Fin  /\  R  e.  _V ) )
201, 19syl 16 . . . . 5  |-  ( ph  ->  ( N  e.  Fin  /\  R  e.  _V )
)
2120simpld 459 . . . 4  |-  ( ph  ->  N  e.  Fin )
22 eqid 2441 . . . . 5  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
2322, 5symgbasfi 16282 . . . 4  |-  ( N  e.  Fin  ->  ( Base `  ( SymGrp `  N
) )  e.  Fin )
2421, 23syl 16 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  e.  Fin )
2516adantr 465 . . . 4  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  R  e.  Ring )
26 zrhpsgnmhm 18490 . . . . . . 7  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
2716, 21, 26syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
289, 12mgpbas 17018 . . . . . . 7  |-  ( Base `  R )  =  (
Base `  (mulGrp `  R
) )
295, 28mhmf 15842 . . . . . 6  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
) : ( Base `  ( SymGrp `  N )
) --> ( Base `  R
) )
3027, 29syl 16 . . . . 5  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) : ( Base `  ( SymGrp `
 N ) ) --> ( Base `  R
) )
3130ffvelrnda 6013 . . . 4  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  e.  ( Base `  R
) )
329crngmgp 17077 . . . . . . 7  |-  ( R  e.  CRing  ->  (mulGrp `  R
)  e. CMnd )
3314, 32syl 16 . . . . . 6  |-  ( ph  ->  (mulGrp `  R )  e. CMnd )
3433adantr 465 . . . . 5  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  (mulGrp `  R )  e. CMnd )
3521adantr 465 . . . . 5  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  N  e.  Fin )
363, 12, 4matbas2i 18794 . . . . . . . . . 10  |-  ( X  e.  B  ->  X  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
371, 36syl 16 . . . . . . . . 9  |-  ( ph  ->  X  e.  ( (
Base `  R )  ^m  ( N  X.  N
) ) )
38 elmapi 7439 . . . . . . . . 9  |-  ( X  e.  ( ( Base `  R )  ^m  ( N  X.  N ) )  ->  X : ( N  X.  N ) --> ( Base `  R
) )
3937, 38syl 16 . . . . . . . 8  |-  ( ph  ->  X : ( N  X.  N ) --> (
Base `  R )
)
4039ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  c  e.  N )  ->  X : ( N  X.  N ) --> ( Base `  R ) )
4122, 5symgbasf1o 16279 . . . . . . . . . 10  |-  ( p  e.  ( Base `  ( SymGrp `
 N ) )  ->  p : N -1-1-onto-> N
)
4241adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  p : N -1-1-onto-> N
)
43 f1of 5803 . . . . . . . . 9  |-  ( p : N -1-1-onto-> N  ->  p : N
--> N )
4442, 43syl 16 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  p : N --> N )
4544ffvelrnda 6013 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  c  e.  N )  ->  (
p `  c )  e.  N )
46 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  c  e.  N )  ->  c  e.  N )
4740, 45, 46fovrnd 6429 . . . . . 6  |-  ( ( ( ph  /\  p  e.  ( Base `  ( SymGrp `
 N ) ) )  /\  c  e.  N )  ->  (
( p `  c
) X c )  e.  ( Base `  R
) )
4847ralrimiva 2855 . . . . 5  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  A. c  e.  N  ( ( p `  c ) X c )  e.  ( Base `  R ) )
4928, 34, 35, 48gsummptcl 16865 . . . 4  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )
5012, 8ringcl 17083 . . . 4  |-  ( ( R  e.  Ring  /\  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  e.  (
Base `  R )  /\  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) )  e.  ( Base `  R
) )
5125, 31, 49, 50syl3anc 1227 . . 3  |-  ( (
ph  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) )  e.  ( Base `  R
) )
52 disjdif 3883 . . . 4  |-  ( (pmEven `  N )  i^i  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )  =  (/)
5352a1i 11 . . 3  |-  ( ph  ->  ( (pmEven `  N
)  i^i  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) )  =  (/) )
5422, 5evpmss 18492 . . . . . 6  |-  (pmEven `  N )  C_  ( Base `  ( SymGrp `  N
) )
55 undif 3891 . . . . . 6  |-  ( (pmEven `  N )  C_  ( Base `  ( SymGrp `  N
) )  <->  ( (pmEven `  N )  u.  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )  =  (
Base `  ( SymGrp `  N ) ) )
5654, 55mpbi 208 . . . . 5  |-  ( (pmEven `  N )  u.  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )  =  (
Base `  ( SymGrp `  N ) )
5756eqcomi 2454 . . . 4  |-  ( Base `  ( SymGrp `  N )
)  =  ( (pmEven `  N )  u.  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
5857a1i 11 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  =  ( (pmEven `  N )  u.  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) ) )
59 eqid 2441 . . 3  |-  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  =  ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
6012, 13, 18, 24, 51, 53, 58, 59gsummptfidmsplitres 16822 . 2  |-  ( ph  ->  ( R  gsumg  ( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) ) )  =  ( ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  (pmEven `  N
) ) ) ( +g  `  R ) ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) ) ) ) )
61 resmpt 5310 . . . . . . 7  |-  ( (pmEven `  N )  C_  ( Base `  ( SymGrp `  N
) )  ->  (
( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  (pmEven `  N )
)  =  ( p  e.  (pmEven `  N
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) ) )
6254, 61ax-mp 5 . . . . . 6  |-  ( ( p  e.  ( Base `  ( SymGrp `  N )
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  (pmEven `  N )
)  =  ( p  e.  (pmEven `  N
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )
6316adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  R  e.  Ring )
6421adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  N  e.  Fin )
65 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  p  e.  (pmEven `  N ) )
66 eqid 2441 . . . . . . . . . . 11  |-  ( 1r
`  R )  =  ( 1r `  R
)
676, 7, 66zrhpsgnevpm 18497 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  N  e.  Fin  /\  p  e.  (pmEven `  N )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p )  =  ( 1r `  R ) )
6863, 64, 65, 67syl3anc 1227 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )  =  ( 1r `  R ) )
6968oveq1d 6293 . . . . . . . 8  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) )  =  ( ( 1r `  R ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )
7054sseli 3483 . . . . . . . . . 10  |-  ( p  e.  (pmEven `  N
)  ->  p  e.  ( Base `  ( SymGrp `  N ) ) )
7170, 49sylan2 474 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )
7212, 8, 66ringlidm 17093 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  (
(mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) )  e.  (
Base `  R )
)  ->  ( ( 1r `  R ) ( .r `  R ) ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )
7363, 71, 72syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( 1r
`  R ) ( .r `  R ) ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )
7469, 73eqtrd 2482 . . . . . . 7  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) )  =  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )
7574mpteq2dva 4520 . . . . . 6  |-  ( ph  ->  ( p  e.  (pmEven `  N )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
7662, 75syl5eq 2494 . . . . 5  |-  ( ph  ->  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  (pmEven `  N
) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
7776oveq2d 6294 . . . 4  |-  ( ph  ->  ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  (pmEven `  N
) ) )  =  ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
78 difss 3614 . . . . . . . 8  |-  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  C_  ( Base `  ( SymGrp `  N )
)
79 resmpt 5310 . . . . . . . 8  |-  ( ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  C_  ( Base `  ( SymGrp `  N
) )  ->  (
( p  e.  (
Base `  ( SymGrp `  N ) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) ) )
8078, 79ax-mp 5 . . . . . . 7  |-  ( ( p  e.  ( Base `  ( SymGrp `  N )
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )
8116adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  ->  R  e.  Ring )
8221adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  ->  N  e.  Fin )
83 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  ->  p  e.  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) )
84 eqid 2441 . . . . . . . . . . . . 13  |-  ( invg `  R )  =  ( invg `  R )
856, 7, 66, 5, 84zrhpsgnodpm 18498 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  N  e.  Fin  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  =  ( ( invg `  R ) `  ( 1r `  R ) ) )
8681, 82, 83, 85syl3anc 1227 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p )  =  ( ( invg `  R ) `  ( 1r `  R ) ) )
8786oveq1d 6293 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( ( ( invg `  R
) `  ( 1r `  R ) ) ( .r `  R ) ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
88 eldifi 3609 . . . . . . . . . . . 12  |-  ( p  e.  ( ( Base `  ( SymGrp `  N )
)  \  (pmEven `  N
) )  ->  p  e.  ( Base `  ( SymGrp `
 N ) ) )
8988, 49sylan2 474 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )
9012, 8, 66, 84, 81, 89ringnegl 17111 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( invg `  R ) `
 ( 1r `  R ) ) ( .r `  R ) ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( ( invg `  R ) `
 ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
9187, 90eqtrd 2482 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( ( invg `  R ) `
 ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
9291mpteq2dva 4520 . . . . . . . 8  |-  ( ph  ->  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( ( invg `  R
) `  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
93 eqidd 2442 . . . . . . . . 9  |-  ( ph  ->  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
94 ringgrp 17074 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  R  e. 
Grp )
9516, 94syl 16 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Grp )
9612, 84grpinvf 15965 . . . . . . . . . . 11  |-  ( R  e.  Grp  ->  ( invg `  R ) : ( Base `  R
) --> ( Base `  R
) )
9795, 96syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( invg `  R ) : (
Base `  R ) --> ( Base `  R )
)
9897feqmptd 5908 . . . . . . . . 9  |-  ( ph  ->  ( invg `  R )  =  ( q  e.  ( Base `  R )  |->  ( ( invg `  R
) `  q )
) )
99 fveq2 5853 . . . . . . . . 9  |-  ( q  =  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  -> 
( ( invg `  R ) `  q
)  =  ( ( invg `  R
) `  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
10089, 93, 98, 99fmptco 6046 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  R )  o.  (
p  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `  N )
)  \  (pmEven `  N
) )  |->  ( ( invg `  R
) `  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
10192, 100eqtr4d 2485 . . . . . . 7  |-  ( ph  ->  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  =  ( ( invg `  R )  o.  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
10280, 101syl5eq 2494 . . . . . 6  |-  ( ph  ->  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) )  =  ( ( invg `  R )  o.  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
103102oveq2d 6294 . . . . 5  |-  ( ph  ->  ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) ) )  =  ( R 
gsumg  ( ( invg `  R )  o.  (
p  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )
104 mdetralt.z . . . . . 6  |-  .0.  =  ( 0g `  R )
105 ringabl 17099 . . . . . . 7  |-  ( R  e.  Ring  ->  R  e. 
Abel )
10616, 105syl 16 . . . . . 6  |-  ( ph  ->  R  e.  Abel )
107 difssd 3615 . . . . . . 7  |-  ( ph  ->  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  C_  ( Base `  ( SymGrp `  N
) ) )
108 ssfi 7739 . . . . . . 7  |-  ( ( ( Base `  ( SymGrp `
 N ) )  e.  Fin  /\  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  C_  ( Base `  ( SymGrp `  N )
) )  ->  (
( Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  e.  Fin )
10924, 107, 108syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  e.  Fin )
110 eqid 2441 . . . . . 6  |-  ( p  e.  ( ( Base `  ( SymGrp `  N )
)  \  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  =  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )
11112, 104, 84, 106, 109, 89, 110gsummptfidminv 16843 . . . . 5  |-  ( ph  ->  ( R  gsumg  ( ( invg `  R )  o.  (
p  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )  =  ( ( invg `  R ) `  ( R  gsumg  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )
11289ralrimiva 2855 . . . . . . . 8  |-  ( ph  ->  A. p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )
113 mdetralt.i . . . . . . . . . . . 12  |-  ( ph  ->  I  e.  N )
114 mdetralt.j . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  N )
115 prssi 4168 . . . . . . . . . . . 12  |-  ( ( I  e.  N  /\  J  e.  N )  ->  { I ,  J }  C_  N )
116113, 114, 115syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  { I ,  J }  C_  N )
117 mdetralt.ij . . . . . . . . . . . 12  |-  ( ph  ->  I  =/=  J )
118 pr2nelem 8382 . . . . . . . . . . . 12  |-  ( ( I  e.  N  /\  J  e.  N  /\  I  =/=  J )  ->  { I ,  J }  ~~  2o )
119113, 114, 117, 118syl3anc 1227 . . . . . . . . . . 11  |-  ( ph  ->  { I ,  J }  ~~  2o )
120 eqid 2441 . . . . . . . . . . . 12  |-  (pmTrsp `  N )  =  (pmTrsp `  N )
121 eqid 2441 . . . . . . . . . . . 12  |-  ran  (pmTrsp `  N )  =  ran  (pmTrsp `  N )
122120, 121pmtrrn 16353 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  { I ,  J }  C_  N  /\  { I ,  J }  ~~  2o )  ->  ( (pmTrsp `  N ) `  {
I ,  J }
)  e.  ran  (pmTrsp `  N ) )
12321, 116, 119, 122syl3anc 1227 . . . . . . . . . 10  |-  ( ph  ->  ( (pmTrsp `  N
) `  { I ,  J } )  e. 
ran  (pmTrsp `  N )
)
12422, 5, 121pmtrodpm 18503 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  ( (pmTrsp `  N ) `  { I ,  J } )  e.  ran  (pmTrsp `  N ) )  ->  ( (pmTrsp `  N ) `  {
I ,  J }
)  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
12521, 123, 124syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( (pmTrsp `  N
) `  { I ,  J } )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
12622, 5evpmodpmf1o 18502 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  ( (pmTrsp `  N ) `  { I ,  J } )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) ) : (pmEven `  N
)
-1-1-onto-> ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
12721, 125, 126syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) ) : (pmEven `  N
)
-1-1-onto-> ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
12812, 18, 109, 112, 110, 127gsummptfif1o 16866 . . . . . . 7  |-  ( ph  ->  ( R  gsumg  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  =  ( R 
gsumg  ( ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  o.  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) ) ) ) )
129 eleq1 2513 . . . . . . . . . . . . 13  |-  ( p  =  q  ->  (
p  e.  (pmEven `  N )  <->  q  e.  (pmEven `  N ) ) )
130129anbi2d 703 . . . . . . . . . . . 12  |-  ( p  =  q  ->  (
( ph  /\  p  e.  (pmEven `  N )
)  <->  ( ph  /\  q  e.  (pmEven `  N
) ) ) )
131 oveq2 6286 . . . . . . . . . . . . 13  |-  ( p  =  q  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p )  =  ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) )
132131eleq1d 2510 . . . . . . . . . . . 12  |-  ( p  =  q  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  <->  ( (
(pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) ) )
133130, 132imbi12d 320 . . . . . . . . . . 11  |-  ( p  =  q  ->  (
( ( ph  /\  p  e.  (pmEven `  N
) )  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p )  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )  <->  ( ( ph  /\  q  e.  (pmEven `  N ) )  -> 
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) ) ) )
13422symggrp 16296 . . . . . . . . . . . . . . 15  |-  ( N  e.  Fin  ->  ( SymGrp `
 N )  e. 
Grp )
13521, 134syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( SymGrp `  N )  e.  Grp )
136135adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( SymGrp `  N
)  e.  Grp )
137121, 22, 5symgtrf 16365 . . . . . . . . . . . . . 14  |-  ran  (pmTrsp `  N )  C_  ( Base `  ( SymGrp `  N
) )
138123adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmTrsp `  N ) `  {
I ,  J }
)  e.  ran  (pmTrsp `  N ) )
139137, 138sseldi 3485 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmTrsp `  N ) `  {
I ,  J }
)  e.  ( Base `  ( SymGrp `  N )
) )
14070adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  p  e.  (
Base `  ( SymGrp `  N ) ) )
141 eqid 2441 . . . . . . . . . . . . . 14  |-  ( +g  `  ( SymGrp `  N )
)  =  ( +g  `  ( SymGrp `  N )
)
1425, 141grpcl 15934 . . . . . . . . . . . . 13  |-  ( ( ( SymGrp `  N )  e.  Grp  /\  ( (pmTrsp `  N ) `  {
I ,  J }
)  e.  ( Base `  ( SymGrp `  N )
)  /\  p  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  (
Base `  ( SymGrp `  N ) ) )
143136, 139, 140, 142syl3anc 1227 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  (
Base `  ( SymGrp `  N ) ) )
144 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( (mulGrp ` fld )s  { 1 ,  -u
1 } )  =  ( (mulGrp ` fld )s  { 1 ,  -u
1 } )
14522, 7, 144psgnghm2 18487 . . . . . . . . . . . . . . . 16  |-  ( N  e.  Fin  ->  (pmSgn `  N )  e.  ( ( SymGrp `  N )  GrpHom  ( (mulGrp ` fld )s  { 1 ,  -u
1 } ) ) )
14621, 145syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (pmSgn `  N )  e.  ( ( SymGrp `  N
)  GrpHom  ( (mulGrp ` fld )s  {
1 ,  -u 1 } ) ) )
147146adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  (pmSgn `  N
)  e.  ( (
SymGrp `  N )  GrpHom  ( (mulGrp ` fld )s  { 1 ,  -u
1 } ) ) )
148 prex 4676 . . . . . . . . . . . . . . . 16  |-  { 1 ,  -u 1 }  e.  _V
149 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
150 cnfldmul 18297 . . . . . . . . . . . . . . . . . 18  |-  x.  =  ( .r ` fld )
151149, 150mgpplusg 17016 . . . . . . . . . . . . . . . . 17  |-  x.  =  ( +g  `  (mulGrp ` fld )
)
152144, 151ressplusg 14613 . . . . . . . . . . . . . . . 16  |-  ( { 1 ,  -u 1 }  e.  _V  ->  x.  =  ( +g  `  (
(mulGrp ` fld )s  { 1 ,  -u
1 } ) ) )
153148, 152ax-mp 5 . . . . . . . . . . . . . . 15  |-  x.  =  ( +g  `  ( (mulGrp ` fld )s  { 1 ,  -u
1 } ) )
1545, 141, 153ghmlin 16143 . . . . . . . . . . . . . 14  |-  ( ( (pmSgn `  N )  e.  ( ( SymGrp `  N
)  GrpHom  ( (mulGrp ` fld )s  {
1 ,  -u 1 } ) )  /\  ( (pmTrsp `  N ) `  { I ,  J } )  e.  (
Base `  ( SymGrp `  N ) )  /\  p  e.  ( Base `  ( SymGrp `  N )
) )  ->  (
(pmSgn `  N ) `  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) )  =  ( ( (pmSgn `  N ) `  (
(pmTrsp `  N ) `  { I ,  J } ) )  x.  ( (pmSgn `  N
) `  p )
) )
155147, 139, 140, 154syl3anc 1227 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmSgn `  N ) `  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p ) )  =  ( ( (pmSgn `  N
) `  ( (pmTrsp `  N ) `  {
I ,  J }
) )  x.  (
(pmSgn `  N ) `  p ) ) )
15622, 121, 7psgnpmtr 16406 . . . . . . . . . . . . . . . 16  |-  ( ( (pmTrsp `  N ) `  { I ,  J } )  e.  ran  (pmTrsp `  N )  -> 
( (pmSgn `  N
) `  ( (pmTrsp `  N ) `  {
I ,  J }
) )  =  -u
1 )
157138, 156syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmSgn `  N ) `  (
(pmTrsp `  N ) `  { I ,  J } ) )  = 
-u 1 )
15822, 5, 7psgnevpm 18495 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  Fin  /\  p  e.  (pmEven `  N
) )  ->  (
(pmSgn `  N ) `  p )  =  1 )
15921, 158sylan 471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmSgn `  N ) `  p
)  =  1 )
160157, 159oveq12d 6296 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( (pmSgn `  N ) `  (
(pmTrsp `  N ) `  { I ,  J } ) )  x.  ( (pmSgn `  N
) `  p )
)  =  ( -u
1  x.  1 ) )
161 neg1cn 10642 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
162161mulid1i 9598 . . . . . . . . . . . . . 14  |-  ( -u
1  x.  1 )  =  -u 1
163160, 162syl6eq 2498 . . . . . . . . . . . . 13  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( (pmSgn `  N ) `  (
(pmTrsp `  N ) `  { I ,  J } ) )  x.  ( (pmSgn `  N
) `  p )
)  =  -u 1
)
164155, 163eqtrd 2482 . . . . . . . . . . . 12  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (pmSgn `  N ) `  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p ) )  =  -u
1 )
16522, 5, 7psgnodpmr 18496 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  (
Base `  ( SymGrp `  N ) )  /\  ( (pmSgn `  N ) `  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) )  = 
-u 1 )  -> 
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
16664, 143, 164, 165syl3anc 1227 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
167133, 166chvarv 1998 . . . . . . . . . 10  |-  ( (
ph  /\  q  e.  (pmEven `  N ) )  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
168 eqidd 2442 . . . . . . . . . 10  |-  ( ph  ->  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) )  =  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) ) )
169 fveq1 5852 . . . . . . . . . . . . 13  |-  ( p  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  ->  (
p `  c )  =  ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) `  c ) )
170169oveq1d 6293 . . . . . . . . . . . 12  |-  ( p  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  ->  (
( p `  c
) X c )  =  ( ( ( ( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) q ) `  c ) X c ) )
171170mpteq2dv 4521 . . . . . . . . . . 11  |-  ( p  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  ->  (
c  e.  N  |->  ( ( p `  c
) X c ) )  =  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
) X c ) ) )
172171oveq2d 6294 . . . . . . . . . 10  |-  ( p  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q )  ->  (
(mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) )  =  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
) X c ) ) ) )
173167, 168, 93, 172fmptco 6046 . . . . . . . . 9  |-  ( ph  ->  ( ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  o.  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) ) )  =  ( q  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) `  c ) X c ) ) ) ) )
174 oveq2 6286 . . . . . . . . . . . . . . 15  |-  ( q  =  p  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) q )  =  ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) p ) )
175174fveq1d 5855 . . . . . . . . . . . . . 14  |-  ( q  =  p  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
)  =  ( ( ( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p ) `  c ) )
176175oveq1d 6293 . . . . . . . . . . . . 13  |-  ( q  =  p  ->  (
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
) X c )  =  ( ( ( ( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p ) `  c ) X c ) )
177176mpteq2dv 4521 . . . . . . . . . . . 12  |-  ( q  =  p  ->  (
c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
) X c ) )  =  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
) X c ) ) )
178177oveq2d 6294 . . . . . . . . . . 11  |-  ( q  =  p  ->  (
(mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) `  c
) X c ) ) )  =  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
) X c ) ) ) )
179178cbvmptv 4525 . . . . . . . . . 10  |-  ( q  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) `  c ) X c ) ) ) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) p ) `  c ) X c ) ) ) )
180179a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( q  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) q ) `  c ) X c ) ) ) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) p ) `  c ) X c ) ) ) ) )
181139adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
(pmTrsp `  N ) `  { I ,  J } )  e.  (
Base `  ( SymGrp `  N ) ) )
182140adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  p  e.  ( Base `  ( SymGrp `
 N ) ) )
18322, 5, 141symgov 16286 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (pmTrsp `  N
) `  { I ,  J } )  e.  ( Base `  ( SymGrp `
 N ) )  /\  p  e.  (
Base `  ( SymGrp `  N ) ) )  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p )  =  ( ( (pmTrsp `  N
) `  { I ,  J } )  o.  p ) )
184181, 182, 183syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p )  =  ( ( (pmTrsp `  N ) `  { I ,  J } )  o.  p
) )
185184fveq1d 5855 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
)  =  ( ( ( (pmTrsp `  N
) `  { I ,  J } )  o.  p ) `  c
) )
18670, 44sylan2 474 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  p : N --> N )
187 fvco3 5932 . . . . . . . . . . . . . . . 16  |-  ( ( p : N --> N  /\  c  e.  N )  ->  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
)  o.  p ) `
 c )  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) )
188186, 187sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
)  o.  p ) `
 c )  =  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) )
189185, 188eqtrd 2482 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
)  =  ( ( (pmTrsp `  N ) `  { I ,  J } ) `  (
p `  c )
) )
190189oveq1d 6293 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
) X c )  =  ( ( ( (pmTrsp `  N ) `  { I ,  J } ) `  (
p `  c )
) X c ) )
191120pmtrprfv 16349 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  Fin  /\  ( I  e.  N  /\  J  e.  N  /\  I  =/=  J
) )  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) `  I )  =  J )
19221, 113, 114, 117, 191syl13anc 1229 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  I )  =  J )
193192ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) `  I )  =  J )
194193oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  I ) X c )  =  ( J X c ) )
195 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  c  e.  N )
196 mdetralt.eq . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. a  e.  N  ( I X a )  =  ( J X a ) )
197196ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  A. a  e.  N  ( I X a )  =  ( J X a ) )
198 oveq2 6286 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  c  ->  (
I X a )  =  ( I X c ) )
199 oveq2 6286 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  c  ->  ( J X a )  =  ( J X c ) )
200198, 199eqeq12d 2463 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  c  ->  (
( I X a )  =  ( J X a )  <->  ( I X c )  =  ( J X c ) ) )
201200rspcv 3190 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  N  ->  ( A. a  e.  N  ( I X a )  =  ( J X a )  -> 
( I X c )  =  ( J X c ) ) )
202195, 197, 201sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
I X c )  =  ( J X c ) )
203194, 202eqtr4d 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  I ) X c )  =  ( I X c ) )
204 fveq2 5853 . . . . . . . . . . . . . . . . 17  |-  ( ( p `  c )  =  I  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) `  ( p `  c
) )  =  ( ( (pmTrsp `  N
) `  { I ,  J } ) `  I ) )
205204oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( ( p `  c )  =  I  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  I ) X c ) )
206 oveq1 6285 . . . . . . . . . . . . . . . 16  |-  ( ( p `  c )  =  I  ->  (
( p `  c
) X c )  =  ( I X c ) )
207205, 206eqeq12d 2463 . . . . . . . . . . . . . . 15  |-  ( ( p `  c )  =  I  ->  (
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c )  <-> 
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  I ) X c )  =  ( I X c ) ) )
208203, 207syl5ibrcom 222 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  =  I  -> 
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) ) )
209 prcom 4090 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { I ,  J }  =  { J ,  I }
210209fveq2i 5856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (pmTrsp `  N ) `  {
I ,  J }
)  =  ( (pmTrsp `  N ) `  { J ,  I }
)
211210fveq1i 5854 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (pmTrsp `  N ) `  { I ,  J } ) `  J
)  =  ( ( (pmTrsp `  N ) `  { J ,  I } ) `  J
)
212117necomd 2712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  J  =/=  I )
213120pmtrprfv 16349 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  Fin  /\  ( J  e.  N  /\  I  e.  N  /\  J  =/=  I
) )  ->  (
( (pmTrsp `  N
) `  { J ,  I } ) `  J )  =  I )
21421, 114, 113, 212, 213syl13anc 1229 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( (pmTrsp `  N ) `  { J ,  I }
) `  J )  =  I )
215211, 214syl5eq 2494 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J )  =  I )
216215oveq1d 6293 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J ) X c )  =  ( I X c ) )
217216ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J ) X c )  =  ( I X c ) )
218217, 202eqtrd 2482 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J ) X c )  =  ( J X c ) )
219 fveq2 5853 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p `  c )  =  J  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) `  ( p `  c
) )  =  ( ( (pmTrsp `  N
) `  { I ,  J } ) `  J ) )
220219oveq1d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( ( p `  c )  =  J  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J ) X c ) )
221 oveq1 6285 . . . . . . . . . . . . . . . . . 18  |-  ( ( p `  c )  =  J  ->  (
( p `  c
) X c )  =  ( J X c ) )
222220, 221eqeq12d 2463 . . . . . . . . . . . . . . . . 17  |-  ( ( p `  c )  =  J  ->  (
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c )  <-> 
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  J ) X c )  =  ( J X c ) ) )
223218, 222syl5ibrcom 222 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  =  J  -> 
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) ) )
224223a1dd 46 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  =  J  -> 
( ( p `  c )  =/=  I  ->  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) ) ) )
225 neanior 2766 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( p `  c
)  =/=  J  /\  ( p `  c
)  =/=  I )  <->  -.  ( ( p `  c )  =  J  \/  ( p `  c )  =  I ) )
226 elpri 4031 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( p `  c )  e.  { I ,  J }  ->  (
( p `  c
)  =  I  \/  ( p `  c
)  =  J ) )
227226orcomd 388 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p `  c )  e.  { I ,  J }  ->  (
( p `  c
)  =  J  \/  ( p `  c
)  =  I ) )
228227con3i 135 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( ( p `  c )  =  J  \/  ( p `  c )  =  I )  ->  -.  (
p `  c )  e.  { I ,  J } )
229225, 228sylbi 195 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( p `  c
)  =/=  J  /\  ( p `  c
)  =/=  I )  ->  -.  ( p `  c )  e.  {
I ,  J }
)
2302293adant1 1013 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  -.  ( p `  c
)  e.  { I ,  J } )
231120pmtrmvd 16352 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  Fin  /\  { I ,  J }  C_  N  /\  { I ,  J }  ~~  2o )  ->  dom  ( (
(pmTrsp `  N ) `  { I ,  J } )  \  _I  )  =  { I ,  J } )
23221, 116, 119, 231syl3anc 1227 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  ( ( (pmTrsp `  N ) `  {
I ,  J }
)  \  _I  )  =  { I ,  J } )
233232ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  dom  ( ( (pmTrsp `  N ) `  {
I ,  J }
)  \  _I  )  =  { I ,  J } )
2342333ad2ant1 1016 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  dom  ( ( (pmTrsp `  N ) `  {
I ,  J }
)  \  _I  )  =  { I ,  J } )
235230, 234neleqtrrd 2554 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  -.  ( p `  c
)  e.  dom  (
( (pmTrsp `  N
) `  { I ,  J } )  \  _I  ) )
236120pmtrf 16351 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  Fin  /\  { I ,  J }  C_  N  /\  { I ,  J }  ~~  2o )  ->  ( (pmTrsp `  N ) `  {
I ,  J }
) : N --> N )
23721, 116, 119, 236syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( (pmTrsp `  N
) `  { I ,  J } ) : N --> N )
238 ffn 5718 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( (pmTrsp `  N ) `  { I ,  J } ) : N --> N  ->  ( (pmTrsp `  N ) `  {
I ,  J }
)  Fn  N )
239237, 238syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( (pmTrsp `  N
) `  { I ,  J } )  Fn  N )
240239ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
(pmTrsp `  N ) `  { I ,  J } )  Fn  N
)
241186ffvelrnda 6013 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
p `  c )  e.  N )
242 fnelnfp 6083 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (pmTrsp `  N
) `  { I ,  J } )  Fn  N  /\  ( p `
 c )  e.  N )  ->  (
( p `  c
)  e.  dom  (
( (pmTrsp `  N
) `  { I ,  J } )  \  _I  )  <->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) )  =/=  ( p `  c
) ) )
243240, 241, 242syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  e.  dom  (
( (pmTrsp `  N
) `  { I ,  J } )  \  _I  )  <->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) )  =/=  ( p `  c
) ) )
2442433ad2ant1 1016 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  (
( p `  c
)  e.  dom  (
( (pmTrsp `  N
) `  { I ,  J } )  \  _I  )  <->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) )  =/=  ( p `  c
) ) )
245244necon2bbid 2697 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) )  =  ( p `  c
)  <->  -.  ( p `  c )  e.  dom  ( ( (pmTrsp `  N ) `  {
I ,  J }
)  \  _I  )
) )
246235, 245mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  (
( (pmTrsp `  N
) `  { I ,  J } ) `  ( p `  c
) )  =  ( p `  c ) )
247246oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  (pmEven `  N
) )  /\  c  e.  N )  /\  (
p `  c )  =/=  J  /\  ( p `
 c )  =/=  I )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) )
2482473exp 1194 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  =/=  J  -> 
( ( p `  c )  =/=  I  ->  ( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) ) ) )
249224, 248pm2.61dne 2758 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( p `  c
)  =/=  I  -> 
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) ) )
250208, 249pm2.61dne 2758 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
I ,  J }
) `  ( p `  c ) ) X c )  =  ( ( p `  c
) X c ) )
251190, 250eqtrd 2482 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  (pmEven `  N )
)  /\  c  e.  N )  ->  (
( ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) p ) `  c
) X c )  =  ( ( p `
 c ) X c ) )
252251mpteq2dva 4520 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N
) `  { I ,  J } ) ( +g  `  ( SymGrp `  N ) ) p ) `  c ) X c ) )  =  ( c  e.  N  |->  ( ( p `
 c ) X c ) ) )
253252oveq2d 6294 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  (pmEven `  N ) )  ->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) p ) `  c ) X c ) ) )  =  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )
254253mpteq2dva 4520 . . . . . . . . 9  |-  ( ph  ->  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( ( ( (pmTrsp `  N ) `  { I ,  J } ) ( +g  `  ( SymGrp `  N )
) p ) `  c ) X c ) ) ) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
255173, 180, 2543eqtrd 2486 . . . . . . . 8  |-  ( ph  ->  ( ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  o.  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) ) )  =  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R
)  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )
256255oveq2d 6294 . . . . . . 7  |-  ( ph  ->  ( R  gsumg  ( ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) )  o.  ( q  e.  (pmEven `  N )  |->  ( ( (pmTrsp `  N ) `  {
I ,  J }
) ( +g  `  ( SymGrp `
 N ) ) q ) ) ) )  =  ( R 
gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
257128, 256eqtrd 2482 . . . . . 6  |-  ( ph  ->  ( R  gsumg  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  =  ( R 
gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )
258257fveq2d 5857 . . . . 5  |-  ( ph  ->  ( ( invg `  R ) `  ( R  gsumg  ( p  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) )  =  ( ( invg `  R ) `  ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )
259103, 111, 2583eqtrd 2486 . . . 4  |-  ( ph  ->  ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) ) )  =  ( ( invg `  R
) `  ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )
26077, 259oveq12d 6296 . . 3  |-  ( ph  ->  ( ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `  N )
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  (pmEven `  N )
) ) ( +g  `  R ) ( R 
gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) ) ) )  =  ( ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ( +g  `  R
) ( ( invg `  R ) `
 ( R  gsumg  ( p  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) ) )
26154a1i 11 . . . . . 6  |-  ( ph  ->  (pmEven `  N )  C_  ( Base `  ( SymGrp `
 N ) ) )
262 ssfi 7739 . . . . . 6  |-  ( ( ( Base `  ( SymGrp `
 N ) )  e.  Fin  /\  (pmEven `  N )  C_  ( Base `  ( SymGrp `  N
) ) )  -> 
(pmEven `  N )  e.  Fin )
26324, 261, 262syl2anc 661 . . . . 5  |-  ( ph  ->  (pmEven `  N )  e.  Fin )
26471ralrimiva 2855 . . . . 5  |-  ( ph  ->  A. p  e.  (pmEven `  N ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) )  e.  ( Base `  R
) )
26512, 18, 263, 264gsummptcl 16865 . . . 4  |-  ( ph  ->  ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  e.  ( Base `  R ) )
26612, 13, 104, 84grprinv 15968 . . . 4  |-  ( ( R  e.  Grp  /\  ( R  gsumg  ( p  e.  (pmEven `  N )  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  e.  ( Base `  R ) )  -> 
( ( R  gsumg  ( p  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ( +g  `  R
) ( ( invg `  R ) `
 ( R  gsumg  ( p  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )  =  .0.  )
26795, 265, 266syl2anc 661 . . 3  |-  ( ph  ->  ( ( R  gsumg  ( p  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ( +g  `  R
) ( ( invg `  R ) `
 ( R  gsumg  ( p  e.  (pmEven `  N
)  |->  ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) ) ) )  =  .0.  )
268260, 267eqtrd 2482 . 2  |-  ( ph  ->  ( ( R  gsumg  ( ( p  e.  ( Base `  ( SymGrp `  N )
)  |->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  p ) ( .r
`  R ) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c
) X c ) ) ) ) )  |`  (pmEven `  N )
) ) ( +g  `  R ) ( R 
gsumg  ( ( p  e.  ( Base `  ( SymGrp `
 N ) ) 
|->  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  p )
( .r `  R
) ( (mulGrp `  R )  gsumg  ( c  e.  N  |->  ( ( p `  c ) X c ) ) ) ) )  |`  ( ( Base `  ( SymGrp `  N
) )  \  (pmEven `  N ) ) ) ) )  =  .0.  )
26911, 60, 2683eqtrd 2486 1  |-  ( ph  ->  ( D `  X
)  =  .0.  )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 972    = wceq 1381    e. wcel 1802    =/= wne 2636   A.wral 2791   _Vcvv 3093    \ cdif 3456    u. cun 3457    i^i cin 3458    C_ wss 3459   (/)c0 3768   {cpr 4013   class class class wbr 4434    |-> cmpt 4492    _I cid 4777    X. cxp 4984   dom cdm 4986   ran crn 4987    |` cres 4988    o. ccom 4990    Fn wfn 5570   -->wf 5571   -1-1-onto->wf1o 5574   ` cfv 5575  (class class class)co 6278   2oc2o 7123    ^m cmap 7419    ~~ cen 7512   Fincfn 7515   1c1 9493    x. cmul 9497   -ucneg 9808   Basecbs 14506   ↾s cress 14507   +g cplusg 14571   .rcmulr 14572   0gc0g 14711    gsumg cgsu 14712   MndHom cmhm 15835   Grpcgrp 15924   invgcminusg 15925    GrpHom cghm 16135   SymGrpcsymg 16273  pmTrspcpmtr 16337  pmSgncpsgn 16385  pmEvencevpm 16386  CMndccmn 16669   Abelcabl 16670  mulGrpcmgp 17012   1rcur 17024   Ringcrg 17069   CRingccrg 17070  ℂfldccnfld 18291   ZRHomczrh 18407   Mat cmat 18779   maDet cmdat 18956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4545  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-addf 9571  ax-mulf 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-xor 1363  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-ot 4020  df-uni 4232  df-int 4269  df-iun 4314  df-iin 4315  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-se 4826  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-isom 5584  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6522  df-om 6683  df-1st 6782  df-2nd 6783  df-supp 6901  df-tpos 6954  df-recs 7041  df-rdg 7075  df-1o 7129  df-2o 7130  df-oadd 7133  df-er 7310  df-map 7421  df-pm 7422  df-ixp 7469  df-en 7516  df-dom 7517  df-sdom 7518  df-fin 7519  df-fsupp 7829  df-sup 7900  df-oi 7935  df-card 8320  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-div 10210  df-nn 10540  df-2 10597  df-3 10598  df-4 10599  df-5 10600  df-6 10601  df-7 10602  df-8 10603  df-9 10604  df-10 10605  df-n0 10799  df-z 10868  df-dec 10982  df-uz 11088  df-rp 11227  df-fz 11679  df-fzo 11801  df-seq 12084  df-exp 12143  df-hash 12382  df-word 12518  df-concat 12520  df-s1 12521  df-substr 12522  df-splice 12523  df-reverse 12524  df-s2 12789  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-starv 14586  df-sca 14587  df-vsca 14588  df-ip 14589  df-tset 14590  df-ple 14591  df-ds 14593  df-unif 14594  df-hom 14595  df-cco 14596  df-0g 14713  df-gsum 14714  df-prds 14719  df-pws 14721  df-mre 14857  df-mrc 14858  df-acs 14860  df-mgm 15743  df-sgrp 15782  df-mnd 15792  df-mhm 15837  df-submnd 15838  df-grp 15928  df-minusg 15929  df-mulg 15931  df-subg 16069  df-ghm 16136  df-gim 16178  df-cntz 16226  df-oppg 16252  df-symg 16274  df-pmtr 16338  df-psgn 16387  df-evpm 16388  df-cmn 16671  df-abl 16672  df-mgp 17013  df-ur 17025  df-ring 17071  df-cring 17072  df-oppr 17143  df-dvdsr 17161  df-unit 17162  df-invr 17192  df-dvr 17203  df-rnghom 17235  df-drng 17269  df-subrg 17298  df-sra 17689  df-rgmod 17690  df-cnfld 18292  df-zring 18360  df-zrh 18411  df-dsmm 18633  df-frlm 18648  df-mat 18780  df-mdet 18957
This theorem is referenced by:  mdetralt2  18981  mdetuni0  18993  mdetmul  18995
  Copyright terms: Public domain W3C validator