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

Theorem mdetunilem7 19643
Description: Lemma for mdetuni 19647. (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 5864 . . . . . 6  |-  ( c  =  d  ->  (
c `  a )  =  ( d `  a ) )
21oveq1d 6305 . . . . 5  |-  ( c  =  d  ->  (
( c `  a
) F b )  =  ( ( d `
 a ) F b ) )
32mpt2eq3dv 6357 . . . 4  |-  ( c  =  d  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( d `  a ) F b ) ) )
43fveq2d 5869 . . 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 5865 . . . 4  |-  ( c  =  d  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d ) )
65oveq1d 6305 . . 3  |-  ( c  =  d  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )
74, 6eqeq12d 2466 . 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 5864 . . . . . 6  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( c `  a )  =  ( ( d ( +g  `  ( SymGrp `  N )
) e ) `  a ) )
98oveq1d 6305 . . . . 5  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
c `  a ) F b )  =  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) )
109mpt2eq3dv 6357 . . . 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 5869 . . 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 5865 . . . 4  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( d ( +g  `  ( SymGrp `  N )
) e ) ) )
1312oveq1d 6305 . . 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 2466 . 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 5864 . . . . . 6  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( c `  a )  =  ( ( 0g `  ( SymGrp `
 N ) ) `
 a ) )
1615oveq1d 6305 . . . . 5  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
c `  a ) F b )  =  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) )
1716mpt2eq3dv 6357 . . . 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 5869 . . 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 5865 . . . 4  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) ) )
2019oveq1d 6305 . . 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 2466 . 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 5864 . . . . . 6  |-  ( c  =  E  ->  (
c `  a )  =  ( E `  a ) )
2322oveq1d 6305 . . . . 5  |-  ( c  =  E  ->  (
( c `  a
) F b )  =  ( ( E `
 a ) F b ) )
2423mpt2eq3dv 6357 . . . 4  |-  ( c  =  E  ->  (
a  e.  N , 
b  e.  N  |->  ( ( c `  a
) F b ) )  =  ( a  e.  N ,  b  e.  N  |->  ( ( E `  a ) F b ) ) )
2524fveq2d 5869 . . 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 5865 . . . 4  |-  ( c  =  E  ->  (
( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  =  ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E ) )
2726oveq1d 6305 . . 3  |-  ( c  =  E  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E )  .x.  ( D `  F )
) )
2825, 27eqeq12d 2466 . 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 2451 . 2  |-  ( 0g
`  ( SymGrp `  N
) )  =  ( 0g `  ( SymGrp `  N ) )
30 eqid 2451 . 2  |-  ( +g  `  ( SymGrp `  N )
)  =  ( +g  `  ( SymGrp `  N )
)
31 eqid 2451 . 2  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
32 mdetuni.n . . . 4  |-  ( ph  ->  N  e.  Fin )
33323ad2ant1 1029 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  N  e.  Fin )
34 eqid 2451 . . . 4  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
3534symggrp 17041 . . 3  |-  ( N  e.  Fin  ->  ( SymGrp `
 N )  e. 
Grp )
36 grpmnd 16678 . . 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 2451 . . . 4  |-  ran  (pmTrsp `  N )  =  ran  (pmTrsp `  N )
3938, 34, 31symgtrf 17110 . . 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 2451 . . . . . 6  |-  (mrCls `  (SubMnd `  ( SymGrp `  N
) ) )  =  (mrCls `  (SubMnd `  ( SymGrp `
 N ) ) )
4238, 34, 31, 41symggen2 17112 . . . . 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 2457 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  =  ( (mrCls `  (SubMnd `  ( SymGrp `  N
) ) ) `  ran  (pmTrsp `  N )
) )
45443ad2ant1 1029 . 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 1029 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  R  e.  Ring )
48 mdetuni.ff . . . . . 6  |-  ( ph  ->  D : B --> K )
49483ad2ant1 1029 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  D : B
--> K )
50 simp3 1010 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  B )
5149, 50ffvelrnd 6023 . . . 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 17804 . . . 4  |-  ( ( R  e.  Ring  /\  ( D `  F )  e.  K )  ->  (  .1.  .x.  ( D `  F ) )  =  ( D `  F
) )
5647, 51, 55syl2anc 667 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  .1.  .x.  ( D `  F
) )  =  ( D `  F ) )
57 zrhpsgnmhm 19152 . . . . . . 7  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
5846, 32, 57syl2anc 667 . . . . . 6  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
59 eqid 2451 . . . . . . . 8  |-  (mulGrp `  R )  =  (mulGrp `  R )
6059, 54ringidval 17737 . . . . . . 7  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
6129, 60mhm0 16590 . . . . . 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 1029 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6463oveq1d 6305 . . 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 17042 . . . . . . . . . . . 12  |-  ( N  e.  Fin  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6632, 65syl 17 . . . . . . . . . . 11  |-  ( ph  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N )
) )
67663ad2ant1 1029 . . . . . . . . . 10  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N ) ) )
68673ad2ant1 1029 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6968fveq1d 5867 . . . . . . . 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 1009 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  a  e.  N )
71 fvresi 6090 . . . . . . . . 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 2487 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
( 0g `  ( SymGrp `
 N ) ) `
 a )  =  a )
7473oveq1d 6305 . . . . . 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 6355 . . . . 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 19447 . . . . . . . 8  |-  ( F  e.  B  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
79783ad2ant3 1031 . . . . . . 7  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
80 elmapi 7493 . . . . . . 7  |-  ( F  e.  ( K  ^m  ( N  X.  N
) )  ->  F : ( N  X.  N ) --> K )
81 ffn 5728 . . . . . . 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 6404 . . . . . 6  |-  ( F  Fn  ( N  X.  N )  <->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8482, 83sylib 200 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  =  ( a  e.  N ,  b  e.  N  |->  ( a F b ) ) )
8575, 84eqtr4d 2488 . . . 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 5869 . . 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 2496 . 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 1009 . . . . . . . . . . . 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 3428 . . . . . . . . . . . . 13  |-  ( e  e.  ran  (pmTrsp `  N )  ->  e  e.  ( Base `  ( SymGrp `
 N ) ) )
90893ad2ant3 1031 . . . . . . . . . . . 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 17031 . . . . . . . . . . . 12  |-  ( ( d  e.  ( Base `  ( SymGrp `  N )
)  /\  e  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( d ( +g  `  ( SymGrp `  N ) ) e )  =  ( d  o.  e ) )
9288, 90, 91syl2anc 667 . . . . . . . . . . 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 5867 . . . . . . . . . 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 1029 . . . . . . . . 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 17024 . . . . . . . . . . . 12  |-  ( e  e.  ( Base `  ( SymGrp `
 N ) )  ->  e : N -1-1-onto-> N
)
96 f1of 5814 . . . . . . . . . . . 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 1029 . . . . . . . . . 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 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
)  ->  a  e.  N )
100 fvco3 5942 . . . . . . . . . 10  |-  ( ( e : N --> N  /\  a  e.  N )  ->  ( ( d  o.  e ) `  a
)  =  ( d `
 ( e `  a ) ) )
10198, 99, 100syl2anc 667 . . . . . . . . 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 2485 . . . . . . . 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 6305 . . . . . . 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 6355 . . . . . 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 5869 . . . . 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 17025 . . . . . 6  |-  ( d  e.  ( Base `  ( SymGrp `
 N ) )  ->  d : N --> N )
107 eqid 2451 . . . . . . . . 9  |-  (pmTrsp `  N )  =  (pmTrsp `  N )
108107, 38pmtrrn2 17101 . . . . . . . 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 1047 . . . . . . . . . . . . . 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 987 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  N  /\  f  e.  N  /\  c  =/=  f )  <->  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )
116115biimpri 210 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f )  ->  (
c  e.  N  /\  f  e.  N  /\  c  =/=  f ) )
117116adantl 468 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  F : ( N  X.  N ) --> K )
120119ad2antrr 732 . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 6023 . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 6441 . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 6023 . . . . . . . . . . . . . . . 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 6441 . . . . . . . . . . . . . . 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 535 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . 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 1029 . . . . . . . . . . . . . . 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 1072 . . . . . . . . . . . . . . . 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 1009 . . . . . . . . . . . . . . . 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 6023 . . . . . . . . . . . . . . 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 1010 . . . . . . . . . . . . . . 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 6441 . . . . . . . . . . . . . 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 19642 . . . . . . . . . . . . 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 1011 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d : N --> N )  ->  ph )
141 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  c  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c ) )
14232adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  N  e.  Fin )
143 simprll 772 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  e.  N )
144 simprlr 773 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  f  e.  N )
145 simprr 766 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  =/=  f )
146107pmtrprfv 17094 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  Fin  /\  ( c  e.  N  /\  f  e.  N  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
147142, 143, 144, 145, 146syl13anc 1270 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
148147adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  c )  =  f )
149141, 148sylan9eqr 2507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  f )
150149fveq2d 5869 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  c
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 f ) )
151150oveq1d 6305 . . . . . . . . . . . . . . . . . . 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 3887 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . 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 2488 . . . . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  f  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a )  =  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f ) )
156 prcom 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { c ,  f }  =  { f ,  c }
157156fveq2i 5868 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (pmTrsp `  N ) `  {
c ,  f } )  =  ( (pmTrsp `  N ) `  {
f ,  c } )
158157fveq1i 5866 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  f
)  =  ( ( (pmTrsp `  N ) `  { f ,  c } ) `  f
)
15932ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  N  e.  Fin )
160 simplrl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( c  e.  N  /\  f  e.  N
) )
161160simprd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  e.  N )
162160simpld 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  e.  N )
163 simplrr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  =/=  f )
164163necomd 2679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  =/=  c )
165107pmtrprfv 17094 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  Fin  /\  ( f  e.  N  /\  c  e.  N  /\  f  =/=  c
) )  ->  (
( (pmTrsp `  N
) `  { f ,  c } ) `
 f )  =  c )
166159, 161, 162, 164, 165syl13anc 1270 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
f ,  c } ) `  f )  =  c )
167158, 166syl5eq 2497 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f )  =  c )
168155, 167sylan9eqr 2507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =  c )
169168fveq2d 5869 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  a  =  f
)  ->  ( d `  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a ) )  =  ( d `
 c ) )
170169oveq1d 6305 . . . . . . . . . . . . . . . . . . . . . 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 3887 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  c ) F b ) )
172171adantl 468 . . . . . . . . . . . . . . . . . . . . . 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 2488 . . . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . 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 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  a  e. 
_V
176175elpr 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  { c ,  f }  <->  ( a  =  c  \/  a  =  f ) )
177176notbii 298 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  a  e.  { c ,  f }  <->  -.  (
a  =  c  \/  a  =  f ) )
178 ioran 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  ( a  =  c  \/  a  =  f )  <->  ( -.  a  =  c  /\  -.  a  =  f ) )
179177, 178bitr2i 254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  <->  -.  a  e.  { c ,  f } )
180179biimpi 198 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
181180adantll 720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
182 prssi 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  N  /\  f  e.  N )  ->  { c ,  f }  C_  N )
183160, 182syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  C_  N )
184 pr2ne 8436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( c  e.  N  /\  f  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
185160, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( { c ,  f }  ~~  2o  <->  c  =/=  f ) )
186163, 185mpbird 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  { c ,  f }  ~~  2o )
187107pmtrmvd 17097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
188159, 183, 186, 187syl3anc 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
189188eleq2d 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
190189notbid 296 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
191190ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
192181, 191mpbird 236 . . . . . . . . . . . . . . . . . . . . . . . 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  )
)
193107pmtrf 17096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  -> 
( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
194159, 183, 186, 193syl3anc 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
195 ffn 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (pmTrsp `  N ) `  { c ,  f } ) : N --> N  ->  ( (pmTrsp `  N ) `  {
c ,  f } )  Fn  N )
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N )
197 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  a  e.  N )
198 fnelnfp 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
a  e.  dom  (
( (pmTrsp `  N
) `  { c ,  f } ) 
\  _I  )  <->  ( (
(pmTrsp `  N ) `  { c ,  f } ) `  a
)  =/=  a ) )
199198necon2bbid 2667 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( (pmTrsp `  N
) `  { c ,  f } )  Fn  N  /\  a  e.  N )  ->  (
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a  <->  -.  a  e.  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )
) )
200196, 197, 199syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . 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  )
) )
201200ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . 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  )
) )
202192, 201mpbird 236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  -> 
( ( (pmTrsp `  N ) `  {
c ,  f } ) `  a )  =  a )
203202fveq2d 5869 . . . . . . . . . . . . . . . . . . . . . 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 ) )
204203oveq1d 6305 . . . . . . . . . . . . . . . . . . . . 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 ) )
205 iffalse 3890 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 c ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
206205adantl 468 . . . . . . . . . . . . . . . . . . . . 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 ) )
207204, 206eqtr4d 2488 . . . . . . . . . . . . . . . . . . . 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 ) ) )
208174, 207pm2.61dan 800 . . . . . . . . . . . . . . . . . . 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 ) ) )
209 iffalse 3890 . . . . . . . . . . . . . . . . . . . 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 ) ) )
210209adantl 468 . . . . . . . . . . . . . . . . . . 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 ) ) )
211208, 210eqtr4d 2488 . . . . . . . . . . . . . . . . . 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 ) ) ) )
212154, 211pm2.61dan 800 . . . . . . . . . . . . . . . . 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 ) ) ) )
2132123adant3 1028 . . . . . . . . . . . . . . . 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 ) ) ) )
214213mpt2eq3dva 6355 . . . . . . . . . . . . . . 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 ) ) ) ) )
215140, 214sylan 474 . . . . . . . . . . . . . 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 ) ) ) ) )
216215fveq2d 5869 . . . . . . . . . . . . 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 ) ) ) ) ) )
217 fveq2 5865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  c  ->  (
d `  a )  =  ( d `  c ) )
218217oveq1d 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  (
( d `  a
) F b )  =  ( ( d `
 c ) F b ) )
219 iftrue 3887 . . . . . . . . . . . . . . . . . . . 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 ) )
220218, 219eqtr4d 2488 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
221 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  f  ->  (
d `  a )  =  ( d `  f ) )
222221oveq1d 6305 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  ( ( d `
 f ) F b ) )
223 iftrue 3887 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  f ) F b ) )
224222, 223eqtr4d 2488 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
225224adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  a  =  f )  ->  ( (
d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
226 iffalse 3890 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
227226eqcomd 2457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  a  =  f  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
228227adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  a  =  c  /\  -.  a  =  f )  ->  (
( d `  a
) F b )  =  if ( a  =  f ,  ( ( d `  f
) F b ) ,  ( ( d `
 a ) F b ) ) )
229225, 228pm2.61dan 800 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
230 iffalse 3890 . . . . . . . . . . . . . . . . . . . 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 ) ) )
231229, 230eqtr4d 2488 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
232220, 231pm2.61i 168 . . . . . . . . . . . . . . . . . 18  |-  ( ( d `  a ) F b )  =  if ( a  =  c ,  ( ( d `  c ) F b ) ,  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
233232a1i 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 ) ) ) )
234233mpt2eq3ia 6356 . . . . . . . . . . . . . . . 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 ) ) ) )
235234fveq2i 5868 . . . . . . . . . . . . . . 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 ) ) ) ) )
236235fveq2i 5868 . . . . . . . . . . . . . 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 ) ) ) ) ) )
237236a1i 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 ) ) ) ) ) ) )
238139, 216, 2373eqtr4d 2495 . . . . . . . . . . . 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 ) ) ) ) )
239 fveq1 5864 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( e `  a )  =  ( ( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) )
240239fveq2d 5869 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( d `  ( e `  a
) )  =  ( d `  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  a
) ) )
241240oveq1d 6305 . . . . . . . . . . . . . . 15  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( (
d `  ( e `  a ) ) F b )  =  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) )
242241mpt2eq3dv 6357 . . . . . . . . . . . . . 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 ) ) )
243242fveq2d 5869 . . . . . . . . . . . . 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 ) ) ) )
244243eqeq1d 2453 . . . . . . . . . . . 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 ) ) ) ) ) )
245238, 244syl5ibrcom 226 . . . . . . . . . . 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 ) ) ) ) ) )
246245expr 620 . . . . . . . . . 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 ) ) ) ) ) ) )
247246impd 433 . . . . . . . . 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 ) ) ) ) ) )
248247rexlimdvva 2886 . . . . . . . 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 ) ) ) ) ) )
249108, 248syl5 33 . . . . . . 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 ) ) ) ) ) )
2502493impia 1205 . . . . . 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 ) ) ) ) )
251106, 250syl3an2 1302 . . . . 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 ) ) ) ) )
252105, 251eqtrd 2485 . . . 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 ) ) ) ) )
253252adantr 467 . . 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 ) ) ) ) )
254 fveq2 5865 . . . 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 )
) ) )
255254adantl 468 . . 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 )
) ) )
256 eqid 2451 . . . . . 6  |-  ( invg `  R )  =  ( invg `  R )
257473ad2ant1 1029 . . . . . 6  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  R  e.  Ring )
258583ad2ant1 1029 . . . . . . . . 9  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
)  e.  ( (
SymGrp `  N ) MndHom  (mulGrp `  R ) ) )
2592583ad2ant1 1029 . . . . . . . 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 )
) )
26059, 52mgpbas 17729 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
26131, 260mhmf 16587 . . . . . . . 8  |-  ( ( ( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
) : ( Base `  ( SymGrp `  N )
) --> K )
262259, 261syl 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 )
263262, 88ffvelrnd 6023 . . . . . 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 )
264493ad2ant1 1029 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  D : B --> K )
265 simp13 1040 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  F  e.  B
)
266264, 265ffvelrnd 6023 . . . . . 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
)
26752, 53, 256, 257, 263, 266ringmneg1 17824 . . . . 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 )
) ) )
26859, 53mgpplusg 17727 . . . . . . . . 9  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
26931, 30, 268mhmlin 16589 . . . . . . . 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 ) ) )
270259, 88, 90, 269syl3anc 1268 . . . . . . 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 ) ) )
271333ad2ant1 1029 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  d  e.  ( Base `  ( SymGrp `
 N ) )  /\  e  e.  ran  (pmTrsp `  N ) )  ->  N  e.  Fin )
272 simp3 1010 . . . . . . . . . 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 ) )
27334, 31, 38pmtrodpm 19165 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  e  e.  ran  (pmTrsp `  N ) )  -> 
e  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
274271, 272, 273syl2anc 667 . . . . . . . . 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
) ) )
275 eqid 2451 . . . . . . . . . 10  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
276 eqid 2451 . . . . . . . . . 10  |-  (pmSgn `  N )  =  (pmSgn `  N )
277275, 276, 54, 31, 256zrhpsgnodpm 19160 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  N  e.  Fin  /\  e  e.  ( ( Base `  ( SymGrp `
 N ) ) 
\  (pmEven `  N
) ) )  -> 
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  e )  =  ( ( invg `  R ) `  .1.  ) )
278257, 271, 274, 277syl3anc 1268 . . . . . . . 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.  ) )
279278oveq2d 6306 . . . . . . 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.  ) ) )
28052, 53, 54, 256, 257, 263rngnegr 17823 . . . . . . 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 ) ) )
281270, 279, 2803eqtrrd 2490 . . . . . 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 ) ) )
282281oveq1d 6305 . . . . 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 ) ) )
283267, 282eqtr3d 2487 . . . 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 ) ) )
284283adantr 467 . . 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 ) ) )
285253, 255, 2843eqtrd 2489 . 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 ) ) )
286 simp2 1009 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E : N
-1-1-onto-> N )
28734, 31elsymgbas 17023 . . . 4  |-  ( N  e.  Fin  ->  ( E  e.  ( Base `  ( SymGrp `  N )
)  <->  E : N -1-1-onto-> N ) )
28833, 287syl 17 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( E  e.  ( Base `  ( SymGrp `
 N ) )  <-> 
E : N -1-1-onto-> N ) )
289286, 288mpbird 236 . 2  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E  e.  ( Base `  ( SymGrp `  N ) ) )
2907, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 285, 289mrcmndind 16613 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 188    \/ wo 370    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887    =/= wne 2622   A.wral 2737   E.wrex 2738    \ cdif 3401    C_ wss 3404   ifcif 3881   {csn 3968   {cpr 3970   class class class wbr 4402    _I cid 4744    X. cxp 4832   dom cdm 4834   ran crn 4835    |` cres 4836    o. ccom 4838    Fn wfn 5577   -->wf 5578   -1-1-onto->wf1o 5581   ` cfv 5582  (class class class)co 6290    |-> cmpt2 6292    oFcof 6529   2oc2o 7176    ^m cmap 7472    ~~ cen 7566   Fincfn 7569   Basecbs 15121   +g cplusg 15190   .rcmulr 15191   0gc0g 15338  mrClscmrc 15489   Mndcmnd 16535   MndHom cmhm 16580  SubMndcsubmnd 16581   Grpcgrp 16669   invgcminusg 16670   SymGrpcsymg 17018  pmTrspcpmtr 17082  pmSgncpsgn 17130  pmEvencevpm 17131  mulGrpcmgp 17723   1rcur 17735   Ringcrg 17780   ZRHomczrh 19071   Mat cmat 19432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598