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

Theorem mdetunilem7 18566
Description: Lemma for mdetuni 18570. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a  |-  A  =  ( N Mat  R )
mdetuni.b  |-  B  =  ( Base `  A
)
mdetuni.k  |-  K  =  ( Base `  R
)
mdetuni.0g  |-  .0.  =  ( 0g `  R )
mdetuni.1r  |-  .1.  =  ( 1r `  R )
mdetuni.pg  |-  .+  =  ( +g  `  R )
mdetuni.tg  |-  .x.  =  ( .r `  R )
mdetuni.n  |-  ( ph  ->  N  e.  Fin )
mdetuni.r  |-  ( ph  ->  R  e.  Ring )
mdetuni.ff  |-  ( ph  ->  D : B --> K )
mdetuni.al  |-  ( ph  ->  A. x  e.  B  A. y  e.  N  A. z  e.  N  ( ( y  =/=  z  /\  A. w  e.  N  ( y
x w )  =  ( z x w ) )  ->  ( D `  x )  =  .0.  ) )
mdetuni.li  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
mdetuni.sc  |-  ( ph  ->  A. x  e.  B  A. y  e.  K  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( ( { w }  X.  N
)  X.  { y } )  oF  .x.  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( y  .x.  ( D `
 z ) ) ) )
Assertion
Ref Expression
mdetunilem7  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  E )  .x.  ( D `  F
) ) )
Distinct variable groups:    ph, x, y, z, w, a, b   
x, B, y, z, w, a, b    x, K, y, z, w, a, b    x, N, y, z, w, a, b   
x, D, y, z, w, a, b    x,  .x. , y, z, w    .+ , a,
b, x, y, z, w    .0. , a, b, x, y, z, w    .1. , a, b, x, y, z, w    x, R, y, z, w    A, a, b, x, y, z, w    x, E, y, z, w    x, F, y, z, w    E, a, b    F, a, b
Allowed substitution hints:    R( a, b)    .x. ( a, b)

Proof of Theorem mdetunilem7
Dummy variables  c 
d  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 5801 . . . . . 6  |-  ( c  =  d  ->  (
c `  a )  =  ( d `  a ) )
21oveq1d 6218 . . . . 5  |-  ( c  =  d  ->  (
( c `  a
) F b )  =  ( ( d `
 a ) F b ) )
32mpt2eq3dv 6264 . . . 4  |-  ( c  =  d  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )
43fveq2d 5806 . . 3  |-  ( c  =  d  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) )
5 fveq2 5802 . . . 4  |-  ( c  =  d  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d ) )
65oveq1d 6218 . . 3  |-  ( c  =  d  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )
74, 6eqeq12d 2476 . 2  |-  ( c  =  d  ->  (
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  <->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( D `  F
) ) ) )
8 fveq1 5801 . . . . . 6  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( c `  a )  =  ( ( d ( +g  `  ( SymGrp `  N )
) e ) `  a ) )
98oveq1d 6218 . . . . 5  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
c `  a ) F b )  =  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) )
109mpt2eq3dv 6264 . . . 4  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) ) )
1110fveq2d 5806 . . 3  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `  a ) F b ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `  N ) ) e ) `  a ) F b ) ) ) )
12 fveq2 5802 . . . 4  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) )
1312oveq1d 6218 . . 3  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) )
1411, 13eqeq12d 2476 . 2  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) ) )  =  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  <->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) ) )
15 fveq1 5801 . . . . . 6  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( c `  a )  =  ( ( 0g `  ( SymGrp `
 N ) ) `
 a ) )
1615oveq1d 6218 . . . . 5  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
c `  a ) F b )  =  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) )
1716mpt2eq3dv 6264 . . . 4  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) ) )
1817fveq2d 5806 . . 3  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `  a ) F b ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  ( ( ( 0g `  ( SymGrp `  N )
) `  a ) F b ) ) ) )
19 fveq2 5802 . . . 4  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) )
2019oveq1d 6218 . . 3  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) 
.x.  ( D `  F ) ) )
2118, 20eqeq12d 2476 . 2  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) ) )  =  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  <->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) 
.x.  ( D `  F ) ) ) )
22 fveq1 5801 . . . . . 6  |-  ( c  =  E  ->  (
c `  a )  =  ( E `  a ) )
2322oveq1d 6218 . . . . 5  |-  ( c  =  E  ->  (
( c `  a
) F b )  =  ( ( E `
 a ) F b ) )
2423mpt2eq3dv 6264 . . . 4  |-  ( c  =  E  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )
2524fveq2d 5806 . . 3  |-  ( c  =  E  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( c `
 a ) F b ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) ) )
26 fveq2 5802 . . . 4  |-  ( c  =  E  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E ) )
2726oveq1d 6218 . . 3  |-  ( c  =  E  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E )  .x.  ( D `  F )
) )
2825, 27eqeq12d 2476 . 2  |-  ( c  =  E  ->  (
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  <->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  E )  .x.  ( D `  F
) ) ) )
29 eqid 2454 . 2  |-  ( 0g
`  ( SymGrp `  N
) )  =  ( 0g `  ( SymGrp `  N ) )
30 eqid 2454 . 2  |-  ( +g  `  ( SymGrp `  N )
)  =  ( +g  `  ( SymGrp `  N )
)
31 eqid 2454 . 2  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
32 mdetuni.n . . . 4  |-  ( ph  ->  N  e.  Fin )
33323ad2ant1 1009 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  N  e.  Fin )
34 eqid 2454 . . . 4  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
3534symggrp 16028 . . 3  |-  ( N  e.  Fin  ->  ( SymGrp `
 N )  e. 
Grp )
36 grpmnd 15673 . . 3  |-  ( (
SymGrp `  N )  e. 
Grp  ->  ( SymGrp `  N
)  e.  Mnd )
3733, 35, 363syl 20 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( SymGrp `  N )  e.  Mnd )
38 eqid 2454 . . . 4  |-  ran  (pmTrsp `  N )  =  ran  (pmTrsp `  N )
3938, 34, 31symgtrf 16098 . . 3  |-  ran  (pmTrsp `  N )  C_  ( Base `  ( SymGrp `  N
) )
4039a1i 11 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ran  (pmTrsp `  N )  C_  ( Base `  ( SymGrp `  N
) ) )
41 eqid 2454 . . . . . 6  |-  (mrCls `  (SubMnd `  ( SymGrp `  N
) ) )  =  (mrCls `  (SubMnd `  ( SymGrp `
 N ) ) )
4238, 34, 31, 41symggen2 16100 . . . . 5  |-  ( N  e.  Fin  ->  (
(mrCls `  (SubMnd `  ( SymGrp `
 N ) ) ) `  ran  (pmTrsp `  N ) )  =  ( Base `  ( SymGrp `
 N ) ) )
4332, 42syl 16 . . . 4  |-  ( ph  ->  ( (mrCls `  (SubMnd `  ( SymGrp `  N )
) ) `  ran  (pmTrsp `  N ) )  =  ( Base `  ( SymGrp `
 N ) ) )
4443eqcomd 2462 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  =  ( (mrCls `  (SubMnd `  ( SymGrp `  N
) ) ) `  ran  (pmTrsp `  N )
) )
45443ad2ant1 1009 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( Base `  ( SymGrp `  N )
)  =  ( (mrCls `  (SubMnd `  ( SymGrp `  N ) ) ) `
 ran  (pmTrsp `  N
) ) )
46 mdetuni.r . . . . 5  |-  ( ph  ->  R  e.  Ring )
47463ad2ant1 1009 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  R  e.  Ring )
48 mdetuni.ff . . . . . 6  |-  ( ph  ->  D : B --> K )
49483ad2ant1 1009 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  D : B
--> K )
50 simp3 990 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  B )
5149, 50ffvelrnd 5956 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( D `  F )  e.  K
)
52 mdetuni.k . . . . 5  |-  K  =  ( Base `  R
)
53 mdetuni.tg . . . . 5  |-  .x.  =  ( .r `  R )
54 mdetuni.1r . . . . 5  |-  .1.  =  ( 1r `  R )
5552, 53, 54rnglidm 16801 . . . 4  |-  ( ( R  e.  Ring  /\  ( D `  F )  e.  K )  ->  (  .1.  .x.  ( D `  F ) )  =  ( D `  F
) )
5647, 51, 55syl2anc 661 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  .1.  .x.  ( D `  F
) )  =  ( D `  F ) )
57 zrhpsgnmhm 18149 . . . . . . 7  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
5846, 32, 57syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
59 eqid 2454 . . . . . . . 8  |-  (mulGrp `  R )  =  (mulGrp `  R )
6059, 54rngidval 16737 . . . . . . 7  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
6129, 60mhm0 15595 . . . . . 6  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6258, 61syl 16 . . . . 5  |-  ( ph  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
63623ad2ant1 1009 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6463oveq1d 6218 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) 
.x.  ( D `  F ) )  =  (  .1.  .x.  ( D `  F )
) )
6534symgid 16029 . . . . . . . . . . . 12  |-  ( N  e.  Fin  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6632, 65syl 16 . . . . . . . . . . 11  |-  ( ph  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N )
) )
67663ad2ant1 1009 . . . . . . . . . 10  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N ) ) )
68673ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6968fveq1d 5804 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
(  _I  |`  N ) `
 a )  =  ( ( 0g `  ( SymGrp `  N )
) `  a )
)
70 simp2 989 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  a  e.  N )
71 fvresi 6016 . . . . . . . . 9  |-  ( a  e.  N  ->  (
(  _I  |`  N ) `
 a )  =  a )
7270, 71syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
(  _I  |`  N ) `
 a )  =  a )
7369, 72eqtr3d 2497 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
( 0g `  ( SymGrp `
 N ) ) `
 a )  =  a )
7473oveq1d 6218 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
( ( 0g `  ( SymGrp `  N )
) `  a ) F b )  =  ( a F b ) )
7574mpt2eq3dva 6262 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g `  ( SymGrp `  N ) ) `  a ) F b ) )  =  ( a  e.  N , 
b  e.  N  |->  ( a F b ) ) )
76 mdetuni.a . . . . . . . . 9  |-  A  =  ( N Mat  R )
77 mdetuni.b . . . . . . . . 9  |-  B  =  ( Base `  A
)
7876, 52, 77matbas2i 18458 . . . . . . . 8  |-  ( F  e.  B  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
79783ad2ant3 1011 . . . . . . 7  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
80 elmapi 7347 . . . . . . 7  |-  ( F  e.  ( K  ^m  ( N  X.  N
) )  ->  F : ( N  X.  N ) --> K )
81 ffn 5670 . . . . . . 7  |-  ( F : ( N  X.  N ) --> K  ->  F  Fn  ( N  X.  N ) )
8279, 80, 813syl 20 . . . . . 6  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  Fn  ( N  X.  N
) )
83 fnov 6311 . . . . . 6  |-  ( F  Fn  ( N  X.  N )  <->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8482, 83sylib 196 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8575, 84eqtr4d 2498 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g `  ( SymGrp `  N ) ) `  a ) F b ) )  =  F )
8685fveq2d 5806 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) ) )  =  ( D `  F ) )
8756, 64, 863eqtr4rd 2506 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) 
.x.  ( D `  F ) ) )
88 simp2 989 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  d  e.  (
Base `  ( SymGrp `  N ) ) )
8939sseli 3463 . . . . . . . . . . . . 13  |-  ( e  e.  ran  (pmTrsp `  N )  ->  e  e.  ( Base `  ( SymGrp `
 N ) ) )
90893ad2ant3 1011 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  e  e.  (
Base `  ( SymGrp `  N ) ) )
9134, 31, 30symgov 16018 . . . . . . . . . . . 12  |-  ( ( d  e.  ( Base `  ( SymGrp `  N )
)  /\  e  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( d ( +g  `  ( SymGrp `  N ) ) e )  =  ( d  o.  e ) )
9288, 90, 91syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( d ( +g  `  ( SymGrp `  N ) ) e )  =  ( d  o.  e ) )
9392fveq1d 5804 . . . . . . . . . 10  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
)  =  ( ( d  o.  e ) `
 a ) )
94933ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( (
d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
)  =  ( ( d  o.  e ) `
 a ) )
9534, 31symgbasf1o 16011 . . . . . . . . . . . 12  |-  ( e  e.  ( Base `  ( SymGrp `
 N ) )  ->  e : N -1-1-onto-> N
)
96 f1of 5752 . . . . . . . . . . . 12  |-  ( e : N -1-1-onto-> N  ->  e : N
--> N )
9790, 95, 963syl 20 . . . . . . . . . . 11  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  e : N --> N )
98973ad2ant1 1009 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  e : N
--> N )
99 simp2 989 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  a  e.  N )
100 fvco3 5880 . . . . . . . . . 10  |-  ( ( e : N --> N  /\  a  e.  N )  ->  ( ( d  o.  e ) `  a
)  =  ( d `
 ( e `  a ) ) )
10198, 99, 100syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( (
d  o.  e ) `
 a )  =  ( d `  (
e `  a )
) )
10294, 101eqtrd 2495 . . . . . . . 8  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( (
d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
)  =  ( d `
 ( e `  a ) ) )
103102oveq1d 6218 . . . . . . 7  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( (
( d ( +g  `  ( SymGrp `  N )
) e ) `  a ) F b )  =  ( ( d `  ( e `
 a ) ) F b ) )
104103mpt2eq3dva 6262 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( a  e.  N ,  b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( e `
 a ) ) F b ) ) )
105104fveq2d 5806 . . . . 5  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( e `
 a ) ) F b ) ) ) )
10634, 31symgbasf1o 16011 . . . . . . 7  |-  ( d  e.  ( Base `  ( SymGrp `
 N ) )  ->  d : N -1-1-onto-> N
)
107 f1of 5752 . . . . . . 7  |-  ( d : N -1-1-onto-> N  ->  d : N
--> N )
108106, 107syl 16 . . . . . 6  |-  ( d  e.  ( Base `  ( SymGrp `
 N ) )  ->  d : N --> N )
109 eqid 2454 . . . . . . . . 9  |-  (pmTrsp `  N )  =  (pmTrsp `  N )
110109, 38pmtrrn2 16089 . . . . . . . 8  |-  ( e  e.  ran  (pmTrsp `  N )  ->  E. c  e.  N  E. f  e.  N  ( c  =/=  f  /\  e  =  ( (pmTrsp `  N ) `  {
c ,  f } ) ) )
111 mdetuni.0g . . . . . . . . . . . . . 14  |-  .0.  =  ( 0g `  R )
112 mdetuni.pg . . . . . . . . . . . . . 14  |-  .+  =  ( +g  `  R )
113 mdetuni.al . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  B  A. y  e.  N  A. z  e.  N  ( ( y  =/=  z  /\  A. w  e.  N  ( y
x w )  =  ( z x w ) )  ->  ( D `  x )  =  .0.  ) )
114 mdetuni.li . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
115 mdetuni.sc . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  B  A. y  e.  K  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( ( { w }  X.  N
)  X.  { y } )  oF  .x.  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( y  .x.  ( D `
 z ) ) ) )
116 simpll1 1027 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  ->  ph )
117 df-3an 967 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  N  /\  f  e.  N  /\  c  =/=  f )  <->  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )
118117biimpri 206 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f )  ->  (
c  e.  N  /\  f  e.  N  /\  c  =/=  f ) )
119118adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( c  e.  N  /\  f  e.  N  /\  c  =/=  f
) )
12079, 80syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F :
( N  X.  N
) --> K )
121120adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  F : ( N  X.  N ) --> K )
122121ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  F : ( N  X.  N ) --> K )
123 simpllr 758 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  d : N --> N )
124 simprlr 762 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
f  e.  N )
125124adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  f  e.  N )
126123, 125ffvelrnd 5956 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  ( d `  f
)  e.  N )
127 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  b  e.  N )
128122, 126, 127fovrnd 6348 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  ( ( d `  f ) F b )  e.  K )
129 simprll 761 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
c  e.  N )
130129adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  c  e.  N )
131123, 130ffvelrnd 5956 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  ( d `  c
)  e.  N )
132122, 131, 127fovrnd 6348 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  ( ( d `  c ) F b )  e.  K )
133128, 132jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  b  e.  N )  ->  ( ( ( d `
 f ) F b )  e.  K  /\  ( ( d `  c ) F b )  e.  K ) )
134120ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  ->  F : ( N  X.  N ) --> K )
1351343ad2ant1 1009 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  F : ( N  X.  N ) --> K )
136 simp1lr 1052 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  d : N --> N )
137 simp2 989 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  a  e.  N )
138136, 137ffvelrnd 5956 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  ( d `  a
)  e.  N )
139 simp3 990 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  b  e.  N )
140135, 138, 139fovrnd 6348 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  ( ( d `  a ) F b )  e.  K )
14176, 77, 52, 111, 54, 112, 53, 32, 46, 48, 113, 114, 115, 116, 119, 133, 140mdetunilem6 18565 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  c ,  ( ( d `
 f ) F b ) ,  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) ) ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) ) ) ) )
142 simpl1 991 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  ph )
143 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  c  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c ) )
14432adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  N  e.  Fin )
145 simprll 761 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  e.  N )
146 simprlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  f  e.  N )
147 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  =/=  f )
148109pmtrprfv 16082 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  Fin  /\  ( c  e.  N  /\  f  e.  N  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
149144, 145, 146, 147, 148syl13anc 1221 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
150149adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c )  =  f )
151143, 150sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  f )
152151fveq2d 5806 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 f ) )
153152oveq1d 6218 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  ( ( d `  f ) F b ) )
154 iftrue 3908 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  if ( a  =  c ,  ( ( d `
 f ) F b ) ,  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) ) )  =  ( ( d `  f
) F b ) )
155154adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  if (
a  =  c ,  ( ( d `  f ) F b ) ,  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )  =  ( ( d `  f ) F b ) )
156153, 155eqtr4d 2498 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  if ( a  =  c ,  ( ( d `  f ) F b ) ,  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) ) )
157 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  f  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f ) )
158 prcom 4064 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { c ,  f }  =  { f ,  c }
159158fveq2i 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (pmTrsp `  N ) `  {
c ,  f } )  =  ( (pmTrsp `  N ) `  {
f ,  c } )
160159fveq1i 5803 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  f
)  =  ( ( (pmTrsp `  N ) `  { f ,  c } ) `  f
)
16132ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  N  e.  Fin )
162 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( c  e.  N  /\  f  e.  N
) )
163162simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  e.  N )
164162simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  e.  N )
165 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  =/=  f )
166165necomd 2723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  =/=  c )
167109pmtrprfv 16082 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  Fin  /\  ( f  e.  N  /\  c  e.  N  /\  f  =/=  c
) )  ->  (
( (pmTrsp `  N
) `  { f ,  c } ) `
 f )  =  c )
168161, 163, 164, 166, 167syl13anc 1221 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
f ,  c } ) `  f )  =  c )
169160, 168syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f )  =  c )
170157, 169sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  c )
171170fveq2d 5806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 c ) )
172171oveq1d 6218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  ( ( d `  c ) F b ) )
173 iftrue 3908 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  c ) F b ) )
174173adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  if (
a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) )  =  ( ( d `
 c ) F b ) )
175172, 174eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )
176175adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  a  =  f )  ->  (
( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b )  =  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )
177 vex 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  a  e. 
_V
178177elpr 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  { c ,  f }  <->  ( a  =  c  \/  a  =  f ) )
179178notbii 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  a  e.  { c ,  f }  <->  -.  (
a  =  c  \/  a  =  f ) )
180 ioran 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  ( a  =  c  \/  a  =  f )  <->  ( -.  a  =  c  /\  -.  a  =  f ) )
181179, 180bitr2i 250 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  <->  -.  a  e.  { c ,  f } )
182181biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
183182adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
184 prssi 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  N  /\  f  e.  N )  ->  { c ,  f }  C_  N )
185162, 184syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  C_  N )
186 pr2ne 8287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( c  e.  N  /\  f  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
187162, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
188165, 187mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  ~~  2o )
189109pmtrmvd 16085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
190161, 185, 188, 189syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
191190eleq2d 2524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  <->  a  e.  { c ,  f } ) )
192191notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( -.  a  e. 
dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  <->  -.  a  e.  { c ,  f } ) )
193192ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( -.  a  e. 
dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  <->  -.  a  e.  { c ,  f } ) )
194183, 193mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
)
195109pmtrf 16084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  -> 
( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
196161, 185, 188, 195syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
197 ffn 5670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) : N --> N  ->  ( (pmTrsp `  N ) `  {
c ,  f } )  Fn  N )
198196, 197syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N )
199 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  a  e.  N )
200 fnelnfp 6020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
a  e.  dom  (
( (pmTrsp `  N
) `  { c ,  f } ) 
\  _I  )  <->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =/=  a ) )
201200necon2bbid 2708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a  <->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
) )
202198, 199, 201syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a  <->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
) )
203202ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a  <->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
) )
204194, 203mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a )
205204fveq2d 5806 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) )  =  ( d `  a ) )
206205oveq1d 6218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b )  =  ( ( d `
 a ) F b ) )
207 iffalse 3910 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
208207adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
209206, 208eqtr4d 2498 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b )  =  if ( a  =  f ,  ( ( d `  c
) F b ) ,  ( ( d `
 a ) F b ) ) )
210176, 209pm2.61dan 789 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )
211 iffalse 3910 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  ->  if ( a  =  c ,  ( ( d `
 f ) F b ) ,  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) ) )  =  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) ) )
212211adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  ->  if (
a  =  c ,  ( ( d `  f ) F b ) ,  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )  =  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) )
213210, 212eqtr4d 2498 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  ->  ( (
d `  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
) ) F b )  =  if ( a  =  c ,  ( ( d `  f ) F b ) ,  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) ) )
214156, 213pm2.61dan 789 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b )  =  if ( a  =  c ,  ( ( d `  f
) F b ) ,  if ( a  =  f ,  ( ( d `  c
) F b ) ,  ( ( d `
 a ) F b ) ) ) )
2152143adant3 1008 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N  /\  b  e.  N )  ->  ( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b )  =  if ( a  =  c ,  ( ( d `  f
) F b ) ,  if ( a  =  f ,  ( ( d `  c
) F b ) ,  ( ( d `
 a ) F b ) ) ) )
216215mpt2eq3dva 6262 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  f
) F b ) ,  if ( a  =  f ,  ( ( d `  c
) F b ) ,  ( ( d `
 a ) F b ) ) ) ) )
217142, 216sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( a  e.  N ,  b  e.  N  |->  ( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  f ) F b ) ,  if ( a  =  f ,  ( ( d `  c ) F b ) ,  ( ( d `  a ) F b ) ) ) ) )
218217fveq2d 5806 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) ) )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  f
) F b ) ,  if ( a  =  f ,  ( ( d `  c
) F b ) ,  ( ( d `
 a ) F b ) ) ) ) ) )
219 fveq2 5802 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  c  ->  (
d `  a )  =  ( d `  c ) )
220219oveq1d 6218 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  (
( d `  a
) F b )  =  ( ( d `
 c ) F b ) )
221 iftrue 3908 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  if ( a  =  c ,  ( ( d `
 c ) F b ) ,  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) ) )  =  ( ( d `  c
) F b ) )
222220, 221eqtr4d 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  c  ->  (
( d `  a
) F b )  =  if ( a  =  c ,  ( ( d `  c
) F b ) ,  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) ) )
223 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  f  ->  (
d `  a )  =  ( d `  f ) )
224223oveq1d 6218 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  ( ( d `
 f ) F b ) )
225 iftrue 3908 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  f ) F b ) )
226224, 225eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
227226adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  a  =  f )  ->  ( (
d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
228 iffalse 3910 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
229228eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
230229adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
231227, 230pm2.61dan 789 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
232 iffalse 3910 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  ->  if ( a  =  c ,  ( ( d `
 c ) F b ) ,  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) ) )  =  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) ) )
233231, 232eqtr4d 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  a  =  c  -> 
( ( d `  a ) F b )  =  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) )
234222, 233pm2.61i 164 . . . . . . . . . . . . . . . . . 18  |-  ( ( d `  a ) F b )  =  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
235234a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( a  e.  N  /\  b  e.  N )  ->  ( ( d `  a ) F b )  =  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) )
236235mpt2eq3ia 6263 . . . . . . . . . . . . . . . 16  |-  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  c
) F b ) ,  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) ) )
237236fveq2i 5805 . . . . . . . . . . . . . . 15  |-  ( D `
 ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) ) )
238237fveq2i 5805 . . . . . . . . . . . . . 14  |-  ( ( invg `  R
) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) ) ) )
239238a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) )  =  ( ( invg `  R
) `  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) ) ) ) ) )
240141, 218, 2393eqtr4d 2505 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) ) )  =  ( ( invg `  R
) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) )
241 fveq1 5801 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( e `  a )  =  ( ( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) )
242241fveq2d 5806 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( d `  ( e `  a
) )  =  ( d `  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  a
) ) )
243242oveq1d 6218 . . . . . . . . . . . . . . 15  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( (
d `  ( e `  a ) ) F b )  =  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) )
244243mpt2eq3dv 6264 . . . . . . . . . . . . . 14  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 ( e `  a ) ) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) ) F b ) ) )
245244fveq2d 5806 . . . . . . . . . . . . 13  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( e `  a
) ) F b ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) ) ) )
246245eqeq1d 2456 . . . . . . . . . . . 12  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 ( e `  a ) ) F b ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) )  <-> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) ) )  =  ( ( invg `  R
) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) ) )
247240, 246syl5ibrcom 222 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  -> 
( e  =  ( (pmTrsp `  N ) `  { c ,  f } )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 ( e `  a ) ) F b ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) ) )
248247expr 615 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( c  e.  N  /\  f  e.  N
) )  ->  (
c  =/=  f  -> 
( e  =  ( (pmTrsp `  N ) `  { c ,  f } )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 ( e `  a ) ) F b ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) ) ) )
249248impd 431 . . . . . . . . 9  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( c  e.  N  /\  f  e.  N
) )  ->  (
( c  =/=  f  /\  e  =  (
(pmTrsp `  N ) `  { c ,  f } ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
e `  a )
) F b ) ) )  =  ( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) ) ) )
250249rexlimdvva 2954 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  -> 
( E. c  e.  N  E. f  e.  N  ( c  =/=  f  /\  e  =  ( (pmTrsp `  N
) `  { c ,  f } ) )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( e `  a
) ) F b ) ) )  =  ( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) ) ) )
251110, 250syl5 32 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  -> 
( e  e.  ran  (pmTrsp `  N )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( d `  (
e `  a )
) F b ) ) )  =  ( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) ) ) )
2522513impia 1185 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N  /\  e  e.  ran  (pmTrsp `  N
) )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 ( e `  a ) ) F b ) ) )  =  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) )
253108, 252syl3an2 1253 . . . . 5  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  ( e `  a
) ) F b ) ) )  =  ( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) ) )
254105, 253eqtrd 2495 . . . 4  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) ) )  =  ( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) ) )
255254adantr 465 . . 3  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( D `  F
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `  N ) ) e ) `  a ) F b ) ) )  =  ( ( invg `  R
) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) ) )
256 fveq2 5802 . . . 4  |-  ( ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
)  ->  ( ( invg `  R ) `
 ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) ) )  =  ( ( invg `  R ) `
 ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) ) )
257256adantl 466 . . 3  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( D `  F
) ) )  -> 
( ( invg `  R ) `  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `
 a ) F b ) ) ) )  =  ( ( invg `  R
) `  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) ) )
258 eqid 2454 . . . . . 6  |-  ( invg `  R )  =  ( invg `  R )
259473ad2ant1 1009 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  R  e.  Ring )
260583ad2ant1 1009 . . . . . . . . 9  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
)  e.  ( (
SymGrp `  N ) MndHom  (mulGrp `  R ) ) )
2612603ad2ant1 1009 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
26259, 52mgpbas 16729 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
26331, 262mhmf 15592 . . . . . . . 8  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
) : ( Base `  ( SymGrp `  N )
) --> K )
264261, 263syl 16 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) : ( Base `  ( SymGrp `
 N ) ) --> K )
265264, 88ffvelrnd 5956 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  e.  K )
266493ad2ant1 1009 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  D : B --> K )
267 simp13 1020 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  F  e.  B
)
268266, 267ffvelrnd 5956 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( D `  F )  e.  K
)
26952, 53, 258, 259, 265, 268rngmneg1 16820 . . . . 5  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( invg `  R
) `  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d ) )  .x.  ( D `  F ) )  =  ( ( invg `  R
) `  ( (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) ) )
27059, 53mgpplusg 16727 . . . . . . . . 9  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
27131, 30, 270mhmlin 15594 . . . . . . . 8  |-  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  /\  d  e.  ( Base `  ( SymGrp `  N ) )  /\  e  e.  ( Base `  ( SymGrp `  N )
) )  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) )  =  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d )  .x.  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e ) ) )
272261, 88, 90, 271syl3anc 1219 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  ( d
( +g  `  ( SymGrp `  N ) ) e ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e ) ) )
273333ad2ant1 1009 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  N  e.  Fin )
274 simp3 990 . . . . . . . . . 10  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  e  e.  ran  (pmTrsp `  N ) )
27534, 31, 38pmtrodpm 18162 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  e  e.  ran  (pmTrsp `  N ) )  -> 
e  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
276273, 274, 275syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  e  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )
277 eqid 2454 . . . . . . . . . 10  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
278 eqid 2454 . . . . . . . . . 10  |-  (pmSgn `  N )  =  (pmSgn `  N )
279277, 278, 54, 31, 258zrhpsgnodpm 18157 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  N  e.  Fin  /\  e  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e )  =  ( ( invg `  R ) `  .1.  ) )
280259, 273, 276, 279syl3anc 1219 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  e )  =  ( ( invg `  R ) `
 .1.  ) )
281280oveq2d 6219 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d )  .x.  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( ( invg `  R ) `  .1.  ) ) )
28252, 53, 54, 258, 259, 265rngnegr 16819 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d )  .x.  (
( invg `  R ) `  .1.  ) )  =  ( ( invg `  R ) `  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d ) ) )
283272, 281, 2823eqtrrd 2500 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( invg `  R ) `
 ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )
)  =  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) )
284283oveq1d 6218 . . . . 5  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( ( invg `  R
) `  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d ) )  .x.  ( D `  F ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) )
285269, 284eqtr3d 2497 . . . 4  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  ( ( invg `  R ) `
 ( ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) )
286285adantr 465 . . 3  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( D `  F
) ) )  -> 
( ( invg `  R ) `  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) )
287255, 257, 2863eqtrd 2499 . 2  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  /\  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  d )  .x.  ( D `  F
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  ( ( ( d ( +g  `  ( SymGrp `  N ) ) e ) `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) 
.x.  ( D `  F ) ) )
288 simp2 989 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E : N
-1-1-onto-> N )
28934, 31elsymgbas 16010 . . . 4  |-  ( N  e.  Fin  ->  ( E  e.  ( Base `  ( SymGrp `  N )
)  <->  E : N -1-1-onto-> N ) )
29033, 289syl 16 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( E  e.  ( Base `  ( SymGrp `
 N ) )  <-> 
E : N -1-1-onto-> N ) )
291288, 290mpbird 232 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E  e.  ( Base `  ( SymGrp `  N ) ) )
2927, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 287, 291mrcmndind 15617 1  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N )
) `  E )  .x.  ( D `  F
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2648   A.wral 2799   E.wrex 2800    \ cdif 3436    C_ wss 3439   ifcif 3902   {csn 3988   {cpr 3990   class class class wbr 4403    _I cid 4742    X. cxp 4949   dom cdm 4951   ran crn 4952    |` cres 4953    o. ccom 4955    Fn wfn 5524   -->wf 5525   -1-1-onto->wf1o 5528   ` cfv 5529  (class class class)co 6203    |-> cmpt2 6205    oFcof 6431   2oc2o 7027    ^m cmap 7327    ~~ cen 7420   Fincfn 7423   Basecbs 14296   +g cplusg 14361   .rcmulr 14362   0gc0g 14501  mrClscmrc 14644   Mndcmnd 15532   Grpcgrp 15533   invgcminusg 15534   MndHom cmhm 15585  SubMndcsubmnd 15586   SymGrpcsymg 16005  pmTrspcpmtr 16070  pmSgncpsgn 16118  pmEvencevpm 16119  mulGrpcmgp 16723   1rcur 16735   Ringcrg 16778   ZRHomczrh 18066   Mat cmat 18415
This theorem was pr