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

Theorem mdetunilem7 19720
Description: Lemma for mdetuni 19724. (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 5878 . . . . . 6  |-  ( c  =  d  ->  (
c `  a )  =  ( d `  a ) )
21oveq1d 6323 . . . . 5  |-  ( c  =  d  ->  (
( c `  a
) F b )  =  ( ( d `
 a ) F b ) )
32mpt2eq3dv 6376 . . . 4  |-  ( c  =  d  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )
43fveq2d 5883 . . 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 5879 . . . 4  |-  ( c  =  d  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d ) )
65oveq1d 6323 . . 3  |-  ( c  =  d  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )
74, 6eqeq12d 2486 . 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 5878 . . . . . 6  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( c `  a )  =  ( ( d ( +g  `  ( SymGrp `  N )
) e ) `  a ) )
98oveq1d 6323 . . . . 5  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
c `  a ) F b )  =  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) )
109mpt2eq3dv 6376 . . . 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 5883 . . 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 5879 . . . 4  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) )
1312oveq1d 6323 . . 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 2486 . 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 5878 . . . . . 6  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( c `  a )  =  ( ( 0g `  ( SymGrp `
 N ) ) `
 a ) )
1615oveq1d 6323 . . . . 5  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
c `  a ) F b )  =  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) )
1716mpt2eq3dv 6376 . . . 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 5883 . . 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 5879 . . . 4  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) )
2019oveq1d 6323 . . 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 2486 . 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 5878 . . . . . 6  |-  ( c  =  E  ->  (
c `  a )  =  ( E `  a ) )
2322oveq1d 6323 . . . . 5  |-  ( c  =  E  ->  (
( c `  a
) F b )  =  ( ( E `
 a ) F b ) )
2423mpt2eq3dv 6376 . . . 4  |-  ( c  =  E  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )
2524fveq2d 5883 . . 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 5879 . . . 4  |-  ( c  =  E  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E ) )
2726oveq1d 6323 . . 3  |-  ( c  =  E  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E )  .x.  ( D `  F )
) )
2825, 27eqeq12d 2486 . 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 2471 . 2  |-  ( 0g
`  ( SymGrp `  N
) )  =  ( 0g `  ( SymGrp `  N ) )
30 eqid 2471 . 2  |-  ( +g  `  ( SymGrp `  N )
)  =  ( +g  `  ( SymGrp `  N )
)
31 eqid 2471 . 2  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
32 mdetuni.n . . . 4  |-  ( ph  ->  N  e.  Fin )
33323ad2ant1 1051 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  N  e.  Fin )
34 eqid 2471 . . . 4  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
3534symggrp 17119 . . 3  |-  ( N  e.  Fin  ->  ( SymGrp `
 N )  e. 
Grp )
36 grpmnd 16756 . . 3  |-  ( (
SymGrp `  N )  e. 
Grp  ->  ( SymGrp `  N
)  e.  Mnd )
3733, 35, 363syl 18 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( SymGrp `  N )  e.  Mnd )
38 eqid 2471 . . . 4  |-  ran  (pmTrsp `  N )  =  ran  (pmTrsp `  N )
3938, 34, 31symgtrf 17188 . . 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 2471 . . . . . 6  |-  (mrCls `  (SubMnd `  ( SymGrp `  N
) ) )  =  (mrCls `  (SubMnd `  ( SymGrp `
 N ) ) )
4238, 34, 31, 41symggen2 17190 . . . . 5  |-  ( N  e.  Fin  ->  (
(mrCls `  (SubMnd `  ( SymGrp `
 N ) ) ) `  ran  (pmTrsp `  N ) )  =  ( Base `  ( SymGrp `
 N ) ) )
4332, 42syl 17 . . . 4  |-  ( ph  ->  ( (mrCls `  (SubMnd `  ( SymGrp `  N )
) ) `  ran  (pmTrsp `  N ) )  =  ( Base `  ( SymGrp `
 N ) ) )
4443eqcomd 2477 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  =  ( (mrCls `  (SubMnd `  ( SymGrp `  N
) ) ) `  ran  (pmTrsp `  N )
) )
45443ad2ant1 1051 . 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 1051 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  R  e.  Ring )
48 mdetuni.ff . . . . . 6  |-  ( ph  ->  D : B --> K )
49483ad2ant1 1051 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  D : B
--> K )
50 simp3 1032 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  B )
5149, 50ffvelrnd 6038 . . . 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, 54ringlidm 17882 . . . 4  |-  ( ( R  e.  Ring  /\  ( D `  F )  e.  K )  ->  (  .1.  .x.  ( D `  F ) )  =  ( D `  F
) )
5647, 51, 55syl2anc 673 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  .1.  .x.  ( D `  F
) )  =  ( D `  F ) )
57 zrhpsgnmhm 19229 . . . . . . 7  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
5846, 32, 57syl2anc 673 . . . . . 6  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
59 eqid 2471 . . . . . . . 8  |-  (mulGrp `  R )  =  (mulGrp `  R )
6059, 54ringidval 17815 . . . . . . 7  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
6129, 60mhm0 16668 . . . . . 6  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6258, 61syl 17 . . . . 5  |-  ( ph  ->  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
63623ad2ant1 1051 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6463oveq1d 6323 . . 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 17120 . . . . . . . . . . . 12  |-  ( N  e.  Fin  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6632, 65syl 17 . . . . . . . . . . 11  |-  ( ph  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N )
) )
67663ad2ant1 1051 . . . . . . . . . 10  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N ) ) )
68673ad2ant1 1051 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6968fveq1d 5881 . . . . . . . 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 1031 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  a  e.  N )
71 fvresi 6106 . . . . . . . . 9  |-  ( a  e.  N  ->  (
(  _I  |`  N ) `
 a )  =  a )
7270, 71syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
(  _I  |`  N ) `
 a )  =  a )
7369, 72eqtr3d 2507 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
( 0g `  ( SymGrp `
 N ) ) `
 a )  =  a )
7473oveq1d 6323 . . . . . 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 6374 . . . . 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 19524 . . . . . . . 8  |-  ( F  e.  B  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
79783ad2ant3 1053 . . . . . . 7  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
80 elmapi 7511 . . . . . . 7  |-  ( F  e.  ( K  ^m  ( N  X.  N
) )  ->  F : ( N  X.  N ) --> K )
81 ffn 5739 . . . . . . 7  |-  ( F : ( N  X.  N ) --> K  ->  F  Fn  ( N  X.  N ) )
8279, 80, 813syl 18 . . . . . 6  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  Fn  ( N  X.  N
) )
83 fnov 6423 . . . . . 6  |-  ( F  Fn  ( N  X.  N )  <->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8482, 83sylib 201 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8575, 84eqtr4d 2508 . . . 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 5883 . . 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 2516 . 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 1031 . . . . . . . . . . . 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 3414 . . . . . . . . . . . . 13  |-  ( e  e.  ran  (pmTrsp `  N )  ->  e  e.  ( Base `  ( SymGrp `
 N ) ) )
90893ad2ant3 1053 . . . . . . . . . . . 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 17109 . . . . . . . . . . . 12  |-  ( ( d  e.  ( Base `  ( SymGrp `  N )
)  /\  e  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( d ( +g  `  ( SymGrp `  N ) ) e )  =  ( d  o.  e ) )
9288, 90, 91syl2anc 673 . . . . . . . . . . 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 5881 . . . . . . . . . 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 1051 . . . . . . . . 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 17102 . . . . . . . . . . . 12  |-  ( e  e.  ( Base `  ( SymGrp `
 N ) )  ->  e : N -1-1-onto-> N
)
96 f1of 5828 . . . . . . . . . . . 12  |-  ( e : N -1-1-onto-> N  ->  e : N
--> N )
9790, 95, 963syl 18 . . . . . . . . . . 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 1051 . . . . . . . . . 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 1031 . . . . . . . . . 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 5957 . . . . . . . . . 10  |-  ( ( e : N --> N  /\  a  e.  N )  ->  ( ( d  o.  e ) `  a
)  =  ( d `
 ( e `  a ) ) )
10198, 99, 100syl2anc 673 . . . . . . . . 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 2505 . . . . . . . 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 6323 . . . . . . 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 6374 . . . . . 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 5883 . . . . 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, 31symgbasf 17103 . . . . . 6  |-  ( d  e.  ( Base `  ( SymGrp `
 N ) )  ->  d : N --> N )
107 eqid 2471 . . . . . . . . 9  |-  (pmTrsp `  N )  =  (pmTrsp `  N )
108107, 38pmtrrn2 17179 . . . . . . . 8  |-  ( e  e.  ran  (pmTrsp `  N )  ->  E. c  e.  N  E. f  e.  N  ( c  =/=  f  /\  e  =  ( (pmTrsp `  N ) `  {
c ,  f } ) ) )
109 mdetuni.0g . . . . . . . . . . . . . 14  |-  .0.  =  ( 0g `  R )
110 mdetuni.pg . . . . . . . . . . . . . 14  |-  .+  =  ( +g  `  R )
111 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.  ) )
112 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 ) ) ) )
113 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 ) ) ) )
114 simpll1 1069 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  ->  ph )
115 df-3an 1009 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  N  /\  f  e.  N  /\  c  =/=  f )  <->  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )
116115biimpri 211 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f )  ->  (
c  e.  N  /\  f  e.  N  /\  c  =/=  f ) )
117116adantl 473 . . . . . . . . . . . . . 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
) )
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F :
( N  X.  N
) --> K )
119118adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  F : ( N  X.  N ) --> K )
120119ad2antrr 740 . . . . . . . . . . . . . . . 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 )
121 simpllr 777 . . . . . . . . . . . . . . . . 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 )
122 simprlr 781 . . . . . . . . . . . . . . . . . 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 )
123122adantr 472 . . . . . . . . . . . . . . . . 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 )
124121, 123ffvelrnd 6038 . . . . . . . . . . . . . . . 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 )
125 simpr 468 . . . . . . . . . . . . . . . 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 )
126120, 124, 125fovrnd 6460 . . . . . . . . . . . . . . 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 )
127 simprll 780 . . . . . . . . . . . . . . . . . 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 )
128127adantr 472 . . . . . . . . . . . . . . . . 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 )
129121, 128ffvelrnd 6038 . . . . . . . . . . . . . . . 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 )
130120, 129, 125fovrnd 6460 . . . . . . . . . . . . . . 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 )
131126, 130jca 541 . . . . . . . . . . . . . 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 ) )
132118ad2antrr 740 . . . . . . . . . . . . . . . 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 )
1331323ad2ant1 1051 . . . . . . . . . . . . . . 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 )
134 simp1lr 1094 . . . . . . . . . . . . . . . 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 )
135 simp2 1031 . . . . . . . . . . . . . . . 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 )
136134, 135ffvelrnd 6038 . . . . . . . . . . . . . . 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 )
137 simp3 1032 . . . . . . . . . . . . . . 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 )
138133, 136, 137fovrnd 6460 . . . . . . . . . . . . . 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 )
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 19719 . . . . . . . . . . . . 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 ) ) ) ) ) ) )
140 simpl1 1033 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  ph )
141 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  c  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c ) )
14232adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  N  e.  Fin )
143 simprll 780 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  e.  N )
144 simprlr 781 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  f  e.  N )
145 simprr 774 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  =/=  f )
146107pmtrprfv 17172 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  Fin  /\  ( c  e.  N  /\  f  e.  N  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
147142, 143, 144, 145, 146syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c )  =  f )
149141, 148sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  f )
150149fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 f ) )
151150oveq1d 6323 . . . . . . . . . . . . . . . . . . 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 ) )
152 iftrue 3878 . . . . . . . . . . . . . . . . . . . 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 ) )
153152adantl 473 . . . . . . . . . . . . . . . . . . 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 ) )
154151, 153eqtr4d 2508 . . . . . . . . . . . . . . . . . 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 ) ) ) )
155 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  f  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f ) )
156 prcom 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { c ,  f }  =  { f ,  c }
157156fveq2i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (pmTrsp `  N ) `  {
c ,  f } )  =  ( (pmTrsp `  N ) `  {
f ,  c } )
158157fveq1i 5880 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  f
)  =  ( ( (pmTrsp `  N ) `  { f ,  c } ) `  f
)
15932ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  N  e.  Fin )
160 simplrl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( c  e.  N  /\  f  e.  N
) )
161160simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  e.  N )
162160simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  e.  N )
163 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  =/=  f )
164163necomd 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  =/=  c )
165107pmtrprfv 17172 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  Fin  /\  ( f  e.  N  /\  c  e.  N  /\  f  =/=  c
) )  ->  (
( (pmTrsp `  N
) `  { f ,  c } ) `
 f )  =  c )
166159, 161, 162, 164, 165syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
f ,  c } ) `  f )  =  c )
167158, 166syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f )  =  c )
168155, 167sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  c )
169168fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 c ) )
170169oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 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 ) )
171 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  c ) F b ) )
172171adantl 473 . . . . . . . . . . . . . . . . . . . . . 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 ) )
173170, 172eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
174173adantlr 729 . . . . . . . . . . . . . . . . . . . 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 ) ) )
175 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  a  e. 
_V
176175elpr 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  e.  { c ,  f }  <->  ( a  =  c  \/  a  =  f ) )
177176notbii 303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  a  e.  { c ,  f }  <->  -.  (
a  =  c  \/  a  =  f ) )
178 ioran 498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  ( a  =  c  \/  a  =  f )  <->  ( -.  a  =  c  /\  -.  a  =  f ) )
179177, 178sylbbr 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
180179adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
181 prssi 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  N  /\  f  e.  N )  ->  { c ,  f }  C_  N )
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  C_  N )
183 pr2ne 8454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( c  e.  N  /\  f  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
185163, 184mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  ~~  2o )
186107pmtrmvd 17175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
187159, 182, 185, 186syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
188187eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
189188notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
190189ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
191180, 190mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 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  )
)
192107pmtrf 17174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  -> 
( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
193159, 182, 185, 192syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
194 ffn 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) : N --> N  ->  ( (pmTrsp `  N ) `  {
c ,  f } )  Fn  N )
195193, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N )
196 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  a  e.  N )
197 fnelnfp 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
a  e.  dom  (
( (pmTrsp `  N
) `  { c ,  f } ) 
\  _I  )  <->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =/=  a ) )
198197necon2bbid 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a  <->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
) )
199195, 196, 198syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 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  )
) )
200199ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 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  )
) )
201191, 200mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a )
202201fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 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 ) )
203202oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 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 ) )
204 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
205204adantl 473 . . . . . . . . . . . . . . . . . . . . 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 ) )
206203, 205eqtr4d 2508 . . . . . . . . . . . . . . . . . . . 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 ) ) )
207174, 206pm2.61dan 808 . . . . . . . . . . . . . . . . . . 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 ) ) )
208 iffalse 3881 . . . . . . . . . . . . . . . . . . . 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 ) ) )
209208adantl 473 . . . . . . . . . . . . . . . . . . 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 ) ) )
210207, 209eqtr4d 2508 . . . . . . . . . . . . . . . . . 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 ) ) ) )
211154, 210pm2.61dan 808 . . . . . . . . . . . . . . . . 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 ) ) ) )
2122113adant3 1050 . . . . . . . . . . . . . . . 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 ) ) ) )
213212mpt2eq3dva 6374 . . . . . . . . . . . . . . 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 ) ) ) ) )
214140, 213sylan 479 . . . . . . . . . . . . . 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 ) ) ) ) )
215214fveq2d 5883 . . . . . . . . . . . . 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 ) ) ) ) ) )
216 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  c  ->  (
d `  a )  =  ( d `  c ) )
217216oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  (
( d `  a
) F b )  =  ( ( d `
 c ) F b ) )
218 iftrue 3878 . . . . . . . . . . . . . . . . . . . 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 ) )
219217, 218eqtr4d 2508 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
220 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  f  ->  (
d `  a )  =  ( d `  f ) )
221220oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  ( ( d `
 f ) F b ) )
222 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  f ) F b ) )
223221, 222eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
224223adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  a  =  f )  ->  ( (
d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
225 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
226225eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
227226adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
228224, 227pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
229 iffalse 3881 . . . . . . . . . . . . . . . . . . . 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 ) ) )
230228, 229eqtr4d 2508 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
231219, 230pm2.61i 169 . . . . . . . . . . . . . . . . . 18  |-  ( ( d `  a ) F b )  =  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
232231a1i 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 ) ) ) )
233232mpt2eq3ia 6375 . . . . . . . . . . . . . . . 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 ) ) ) )
234233fveq2i 5882 . . . . . . . . . . . . . . 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 ) ) ) ) )
235234fveq2i 5882 . . . . . . . . . . . . . 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 ) ) ) ) ) )
236235a1i 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 ) ) ) ) ) ) )
237139, 215, 2363eqtr4d 2515 . . . . . . . . . . . 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 ) ) ) ) )
238 fveq1 5878 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( e `  a )  =  ( ( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) )
239238fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( d `  ( e `  a
) )  =  ( d `  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  a
) ) )
240239oveq1d 6323 . . . . . . . . . . . . . . 15  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( (
d `  ( e `  a ) ) F b )  =  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) )
241240mpt2eq3dv 6376 . . . . . . . . . . . . . 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 ) ) )
242241fveq2d 5883 . . . . . . . . . . . . 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 ) ) ) )
243242eqeq1d 2473 . . . . . . . . . . . 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 ) ) ) ) ) )
244237, 243syl5ibrcom 230 . . . . . . . . . . 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 ) ) ) ) ) )
245244expr 626 . . . . . . . . . 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 ) ) ) ) ) ) )
246245impd 438 . . . . . . . . 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 ) ) ) ) ) )
247246rexlimdvva 2878 . . . . . . . 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 ) ) ) ) ) )
248108, 247syl5 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 ) ) ) ) ) )
2492483impia 1228 . . . . . 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 ) ) ) ) )
250106, 249syl3an2 1326 . . . . 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 ) ) ) ) )
251105, 250eqtrd 2505 . . . 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 ) ) ) ) )
252251adantr 472 . . 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 ) ) ) ) )
253 fveq2 5879 . . . 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 )
) ) )
254253adantl 473 . . 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 )
) ) )
255 eqid 2471 . . . . . 6  |-  ( invg `  R )  =  ( invg `  R )
256473ad2ant1 1051 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  R  e.  Ring )
257583ad2ant1 1051 . . . . . . . . 9  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
)  e.  ( (
SymGrp `  N ) MndHom  (mulGrp `  R ) ) )
2582573ad2ant1 1051 . . . . . . . 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 )
) )
25959, 52mgpbas 17807 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
26031, 259mhmf 16665 . . . . . . . 8  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
) : ( Base `  ( SymGrp `  N )
) --> K )
261258, 260syl 17 . . . . . . 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 )
262261, 88ffvelrnd 6038 . . . . . 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 )
263493ad2ant1 1051 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  D : B --> K )
264 simp13 1062 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  F  e.  B
)
265263, 264ffvelrnd 6038 . . . . . 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
)
26652, 53, 255, 256, 262, 265ringmneg1 17902 . . . . 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 )
) ) )
26759, 53mgpplusg 17805 . . . . . . . . 9  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
26831, 30, 267mhmlin 16667 . . . . . . . 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 ) ) )
269258, 88, 90, 268syl3anc 1292 . . . . . . 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 ) ) )
270333ad2ant1 1051 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  N  e.  Fin )
271 simp3 1032 . . . . . . . . . 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 ) )
27234, 31, 38pmtrodpm 19242 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  e  e.  ran  (pmTrsp `  N ) )  -> 
e  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
273270, 271, 272syl2anc 673 . . . . . . . . 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
) ) )
274 eqid 2471 . . . . . . . . . 10  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
275 eqid 2471 . . . . . . . . . 10  |-  (pmSgn `  N )  =  (pmSgn `  N )
276274, 275, 54, 31, 255zrhpsgnodpm 19237 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  N  e.  Fin  /\  e  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e )  =  ( ( invg `  R ) `  .1.  ) )
277256, 270, 273, 276syl3anc 1292 . . . . . . . 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.  ) )
278277oveq2d 6324 . . . . . . 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.  ) ) )
27952, 53, 54, 255, 256, 262rngnegr 17901 . . . . . . 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 ) ) )
280269, 278, 2793eqtrrd 2510 . . . . . 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 ) ) )
281280oveq1d 6323 . . . . 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 ) ) )
282266, 281eqtr3d 2507 . . . 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 ) ) )
283282adantr 472 . . 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 ) ) )
284252, 254, 2833eqtrd 2509 . 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 ) ) )
285 simp2 1031 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E : N
-1-1-onto-> N )
28634, 31elsymgbas 17101 . . . 4  |-  ( N  e.  Fin  ->  ( E  e.  ( Base `  ( SymGrp `  N )
)  <->  E : N -1-1-onto-> N ) )
28733, 286syl 17 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( E  e.  ( Base `  ( SymGrp `
 N ) )  <-> 
E : N -1-1-onto-> N ) )
288285, 287mpbird 240 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E  e.  ( Base `  ( SymGrp `  N ) ) )
2897, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 284, 288mrcmndind 16691 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 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757    \ cdif 3387    C_ wss 3390   ifcif 3872   {csn 3959   {cpr 3961   class class class wbr 4395    _I cid 4749    X. cxp 4837   dom cdm 4839   ran crn 4840    |` cres 4841    o. ccom 4843    Fn wfn 5584   -->wf 5585   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308    |-> cmpt2 6310    oFcof 6548   2oc2o 7194    ^m cmap 7490    ~~ cen 7584   Fincfn 7587   Basecbs 15199   +g cplusg 15268   .rcmulr 15269   0gc0g 15416  mrClscmrc 15567   Mndcmnd 16613   MndHom cmhm 16658  SubMndcsubmnd 16659   Grpcgrp 16747   invgcminusg 16748   SymGrpcsymg 17096  pmTrspcpmtr 17160  pmSgncpsgn 17208  pmEvencevpm 17209  mulGrpcmgp 17801   1rcur 17813   Ringcrg 17858   ZRHomczrh 19148   Mat cmat 19509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0