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

Theorem mdetunilem7 19635
Description: Lemma for mdetuni 19639. (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 6318 . . . . 5  |-  ( c  =  d  ->  (
( c `  a
) F b )  =  ( ( d `
 a ) F b ) )
32mpt2eq3dv 6369 . . . 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 6318 . . 3  |-  ( c  =  d  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  d )  .x.  ( D `  F )
) )
74, 6eqeq12d 2445 . 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 6318 . . . . 5  |-  ( c  =  ( d ( +g  `  ( SymGrp `  N ) ) e )  ->  ( (
c `  a ) F b )  =  ( ( ( d ( +g  `  ( SymGrp `
 N ) ) e ) `  a
) F b ) )
109mpt2eq3dv 6369 . . . 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 6318 . . 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 2445 . 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 6318 . . . . 5  |-  ( c  =  ( 0g `  ( SymGrp `  N )
)  ->  ( (
c `  a ) F b )  =  ( ( ( 0g
`  ( SymGrp `  N
) ) `  a
) F b ) )
1716mpt2eq3dv 6369 . . . 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 6318 . . 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 2445 . 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 6318 . . . . 5  |-  ( c  =  E  ->  (
( c `  a
) F b )  =  ( ( E `
 a ) F b ) )
2423mpt2eq3dv 6369 . . . 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 6318 . . 3  |-  ( c  =  E  ->  (
( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  c )  .x.  ( D `  F )
)  =  ( ( ( ( ZRHom `  R )  o.  (pmSgn `  N ) ) `  E )  .x.  ( D `  F )
) )
2825, 27eqeq12d 2445 . 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 2423 . 2  |-  ( 0g
`  ( SymGrp `  N
) )  =  ( 0g `  ( SymGrp `  N ) )
30 eqid 2423 . 2  |-  ( +g  `  ( SymGrp `  N )
)  =  ( +g  `  ( SymGrp `  N )
)
31 eqid 2423 . 2  |-  ( Base `  ( SymGrp `  N )
)  =  ( Base `  ( SymGrp `  N )
)
32 mdetuni.n . . . 4  |-  ( ph  ->  N  e.  Fin )
33323ad2ant1 1027 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  N  e.  Fin )
34 eqid 2423 . . . 4  |-  ( SymGrp `  N )  =  (
SymGrp `  N )
3534symggrp 17034 . . 3  |-  ( N  e.  Fin  ->  ( SymGrp `
 N )  e. 
Grp )
36 grpmnd 16671 . . 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 2423 . . . 4  |-  ran  (pmTrsp `  N )  =  ran  (pmTrsp `  N )
3938, 34, 31symgtrf 17103 . . 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 2423 . . . . . 6  |-  (mrCls `  (SubMnd `  ( SymGrp `  N
) ) )  =  (mrCls `  (SubMnd `  ( SymGrp `
 N ) ) )
4238, 34, 31, 41symggen2 17105 . . . . 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 2431 . . 3  |-  ( ph  ->  ( Base `  ( SymGrp `
 N ) )  =  ( (mrCls `  (SubMnd `  ( SymGrp `  N
) ) ) `  ran  (pmTrsp `  N )
) )
45443ad2ant1 1027 . 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 1027 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  R  e.  Ring )
48 mdetuni.ff . . . . . 6  |-  ( ph  ->  D : B --> K )
49483ad2ant1 1027 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  D : B
--> K )
50 simp3 1008 . . . . 5  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  B )
5149, 50ffvelrnd 6036 . . . 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 17797 . . . 4  |-  ( ( R  e.  Ring  /\  ( D `  F )  e.  K )  ->  (  .1.  .x.  ( D `  F ) )  =  ( D `  F
) )
5647, 51, 55syl2anc 666 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  .1.  .x.  ( D `  F
) )  =  ( D `  F ) )
57 zrhpsgnmhm 19144 . . . . . . 7  |-  ( ( R  e.  Ring  /\  N  e.  Fin )  ->  (
( ZRHom `  R
)  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
5846, 32, 57syl2anc 666 . . . . . 6  |-  ( ph  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N ) )  e.  ( ( SymGrp `  N
) MndHom  (mulGrp `  R )
) )
59 eqid 2423 . . . . . . . 8  |-  (mulGrp `  R )  =  (mulGrp `  R )
6059, 54ringidval 17730 . . . . . . 7  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
6129, 60mhm0 16583 . . . . . 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 1027 . . . 4  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( (
( ZRHom `  R
)  o.  (pmSgn `  N ) ) `  ( 0g `  ( SymGrp `  N ) ) )  =  .1.  )
6463oveq1d 6318 . . 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 17035 . . . . . . . . . . . 12  |-  ( N  e.  Fin  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `
 N ) ) )
6632, 65syl 17 . . . . . . . . . . 11  |-  ( ph  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N )
) )
67663ad2ant1 1027 . . . . . . . . . 10  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  (  _I  |`  N )  =  ( 0g `  ( SymGrp `  N ) ) )
68673ad2ant1 1027 . . . . . . . . 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 1007 . . . . . . . . 9  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  a  e.  N )
71 fvresi 6103 . . . . . . . . 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 2466 . . . . . . 7  |-  ( ( ( ph  /\  E : N -1-1-onto-> N  /\  F  e.  B )  /\  a  e.  N  /\  b  e.  N )  ->  (
( 0g `  ( SymGrp `
 N ) ) `
 a )  =  a )
7473oveq1d 6318 . . . . . 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 6367 . . . . 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 19439 . . . . . . . 8  |-  ( F  e.  B  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
79783ad2ant3 1029 . . . . . . 7  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  F  e.  ( K  ^m  ( N  X.  N ) ) )
80 elmapi 7499 . . . . . . 7  |-  ( F  e.  ( K  ^m  ( N  X.  N
) )  ->  F : ( N  X.  N ) --> K )
81 ffn 5744 . . . . . . 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 6416 . . . . . 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 2467 . . . 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 2475 . 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 1007 . . . . . . . . . . . 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 3461 . . . . . . . . . . . . 13  |-  ( e  e.  ran  (pmTrsp `  N )  ->  e  e.  ( Base `  ( SymGrp `
 N ) ) )
90893ad2ant3 1029 . . . . . . . . . . . 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 17024 . . . . . . . . . . . 12  |-  ( ( d  e.  ( Base `  ( SymGrp `  N )
)  /\  e  e.  ( Base `  ( SymGrp `  N ) ) )  ->  ( d ( +g  `  ( SymGrp `  N ) ) e )  =  ( d  o.  e ) )
9288, 90, 91syl2anc 666 . . . . . . . . . . 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 1027 . . . . . . . . 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 17017 . . . . . . . . . . . 12  |-  ( e  e.  ( Base `  ( SymGrp `
 N ) )  ->  e : N -1-1-onto-> N
)
96 f1of 5829 . . . . . . . . . . . 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 1027 . . . . . . . . . 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 1007 . . . . . . . . . 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 5956 . . . . . . . . . 10  |-  ( ( e : N --> N  /\  a  e.  N )  ->  ( ( d  o.  e ) `  a
)  =  ( d `
 ( e `  a ) ) )
10198, 99, 100syl2anc 666 . . . . . . . . 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 2464 . . . . . . . 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 6318 . . . . . . 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 6367 . . . . . 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 17018 . . . . . 6  |-  ( d  e.  ( Base `  ( SymGrp `
 N ) )  ->  d : N --> N )
107 eqid 2423 . . . . . . . . 9  |-  (pmTrsp `  N )  =  (pmTrsp `  N )
108107, 38pmtrrn2 17094 . . . . . . . 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 1045 . . . . . . . . . . . . . 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 985 . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . . 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 6453 . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . . 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 6453 . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . 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 1027 . . . . . . . . . . . . . . 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 1070 . . . . . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . 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 1008 . . . . . . . . . . . . . . 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 6453 . . . . . . . . . . . . . 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 19634 . . . . . . . . . . . . 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 1009 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  N  e.  Fin )
143 simprll 771 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  e.  N )
144 simprlr 772 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  f  e.  N )
145 simprr 765 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( (
c  e.  N  /\  f  e.  N )  /\  c  =/=  f
) )  ->  c  =/=  f )
146107pmtrprfv 17087 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  Fin  /\  ( c  e.  N  /\  f  e.  N  /\  c  =/=  f
) )  ->  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 c )  =  f )
147142, 143, 144, 145, 146syl13anc 1267 . . . . . . . . . . . . . . . . . . . . . . 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 2486 . . . . . . . . . . . . . . . . . . . . 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 6318 . . . . . . . . . . . . . . . . . . 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 3916 . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . 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 4076 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  N  e.  Fin )
160 simplrl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  c  =/=  f )
164163necomd 2696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  f  =/=  c )
165107pmtrprfv 17087 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  Fin  /\  ( f  e.  N  /\  c  e.  N  /\  f  =/=  c
) )  ->  (
( (pmTrsp `  N
) `  { f ,  c } ) `
 f )  =  c )
166159, 161, 162, 164, 165syl13anc 1267 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
f ,  c } ) `  f )  =  c )
167158, 166syl5eq 2476 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( ( (pmTrsp `  N ) `  {
c ,  f } ) `  f )  =  c )
168155, 167sylan9eqr 2486 . . . . . . . . . . . . . . . . . . . . . . . 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 6318 . . . . . . . . . . . . . . . . . . . . . 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 3916 . . . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . 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 3085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  a  e. 
_V
176175elpr 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( ( c  e.  N  /\  f  e.  N )  /\  c  =/=  f ) )  /\  a  e.  N )  /\  -.  a  =  c )  /\  -.  a  =  f )  ->  -.  a  e.  { c ,  f } )
182 prssi 4154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
188159, 183, 186, 187syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  dom  ( ( (pmTrsp `  N ) `  {
c ,  f } )  \  _I  )  =  { c ,  f } )
189188eleq2d 2493 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . 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 17089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  Fin  /\  { c ,  f } 
C_  N  /\  {
c ,  f } 
~~  2o )  -> 
( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
194159, 183, 186, 193syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
( c  e.  N  /\  f  e.  N
)  /\  c  =/=  f ) )  /\  a  e.  N )  ->  ( (pmTrsp `  N
) `  { c ,  f } ) : N --> N )
195 ffn 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2681 . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) )
204203oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 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 3919 . . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . . . 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 3919 . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . 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 6367 . . . . . . . . . . . . . . 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 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 ) ) ) ) ) )
217 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  c  ->  (
d `  a )  =  ( d `  c ) )
218217oveq1d 6318 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  c  ->  (
( d `  a
) F b )  =  ( ( d `
 c ) F b ) )
219 iftrue 3916 . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  f  ->  (
d `  a )  =  ( d `  f ) )
222221oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  (
( d `  a
) F b )  =  ( ( d `
 f ) F b ) )
223 iftrue 3916 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  f ) F b ) )
224222, 223eqtr4d 2467 . . . . . . . . . . . . . . . . . . . . . 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 3919 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  a  =  f  ->  if ( a  =  f ,  ( ( d `
 f ) F b ) ,  ( ( d `  a
) F b ) )  =  ( ( d `  a ) F b ) )
227226eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  =  c  -> 
( ( d `  a ) F b )  =  if ( a  =  f ,  ( ( d `  f ) F b ) ,  ( ( d `  a ) F b ) ) )
230 iffalse 3919 . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . 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 6368 . . . . . . . . . . . . . . . 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 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 ) ) ) ) )
236235fveq2i 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 ) ) ) ) ) )
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 2474 . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( e `  a )  =  ( ( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) )
240239fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( d `  ( e `  a
) )  =  ( d `  ( ( (pmTrsp `  N ) `  { c ,  f } ) `  a
) ) )
241240oveq1d 6318 . . . . . . . . . . . . . . 15  |-  ( e  =  ( (pmTrsp `  N ) `  {
c ,  f } )  ->  ( (
d `  ( e `  a ) ) F b )  =  ( ( d `  (
( (pmTrsp `  N
) `  { c ,  f } ) `
 a ) ) F b ) )
242241mpt2eq3dv 6369 . . . . . . . . . . . . . 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 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 ) ) ) )
244243eqeq1d 2425 . . . . . . . . . . . 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 619 . . . . . . . . . 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 2925 . . . . . . . 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 34 . . . . . . 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 1203 . . . . . 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 1299 . . . . 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 2464 . . . 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 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 )
) ) )
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 2423 . . . . . 6  |-  ( invg `  R )  =  ( invg `  R )
257473ad2ant1 1027 . . . . . 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 1027 . . . . . . . . 9  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  ( ( ZRHom `  R )  o.  (pmSgn `  N )
)  e.  ( (
SymGrp `  N ) MndHom  (mulGrp `  R ) ) )
2592583ad2ant1 1027 . . . . . . . 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 17722 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
26131, 260mhmf 16580 . . . . . . . 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 6036 . . . . . 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 1027 . . . . . . 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 1038 . . . . . . 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 6036 . . . . . 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 17817 . . . . 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 17720 . . . . . . . . 9  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
26931, 30, 268mhmlin 16582 . . . . . . . 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 1265 . . . . . . 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 1027 . . . . . . . . 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 1008 . . . . . . . . . 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 19157 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  e  e.  ran  (pmTrsp `  N ) )  -> 
e  e.  ( (
Base `  ( SymGrp `  N ) )  \ 
(pmEven `  N )
) )
274271, 272, 273syl2anc 666 . . . . . . . . 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 2423 . . . . . . . . . 10  |-  ( ZRHom `  R )  =  ( ZRHom `  R )
276 eqid 2423 . . . . . . . . . 10  |-  (pmSgn `  N )  =  (pmSgn `  N )
277275, 276, 54, 31, 256zrhpsgnodpm 19152 . . . . . . . . 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 1265 . . . . . . . 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 6319 . . . . . . 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 17816 . . . . . . 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 2469 . . . . . 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 6318 . . . . 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 2466 . . . 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 2468 . 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 1007 . . 3  |-  ( (
ph  /\  E : N
-1-1-onto-> N  /\  F  e.  B
)  ->  E : N
-1-1-onto-> N )
28734, 31elsymgbas 17016 . . . 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 16606 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 983    = wceq 1438    e. wcel 1869    =/= wne 2619   A.wral 2776   E.wrex 2777    \ cdif 3434    C_ wss 3437   ifcif 3910   {csn 3997   {cpr 3999   class class class wbr 4421    _I cid 4761    X. cxp 4849   dom cdm 4851   ran crn 4852    |` cres 4853    o. ccom 4855    Fn wfn 5594   -->wf 5595   -1-1-onto->wf1o 5598   ` cfv 5599  (class class class)co 6303    |-> cmpt2 6305    oFcof 6541   2oc2o 7182    ^m cmap 7478    ~~ cen 7572   Fincfn 7575   Basecbs 15114   +g cplusg 15183   .rcmulr 15184   0gc0g 15331  mrClscmrc 15482   Mndcmnd 16528   MndHom cmhm 16573  SubMndcsubmnd 16574   Grpcgrp 16662   invgcminusg 16663   SymGrpcsymg 17011  pmTrspcpmtr 17075  pmSgncpsgn 17123  pmEvencevpm 17124  mulGrpcmgp 17716   1rcur 17728   Ringcrg 17773   ZRHomczrh 19063   Mat cmat 19424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl