Metamath Proof Explorer

Theorem mdetunilem7

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 mdetuni.a 
 |-  A = ( N Mat R )
2 mdetuni.b 
 |-  B = ( Base ` A )
3 mdetuni.k 
 |-  K = ( Base ` R )
4 mdetuni.0g 
 |-  .0. = ( 0g ` R )
5 mdetuni.1r 
 |-  .1. = ( 1r ` R )
6 mdetuni.pg 
 |-  .+ = ( +g ` R )
7 mdetuni.tg 
 |-  .x. = ( .r ` R )
8 mdetuni.n 
 |-  ( ph -> N e. Fin )
9 mdetuni.r 
 |-  ( ph -> R e. Ring )
10 mdetuni.ff 
 |-  ( ph -> D : B --> K )
11 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. ) )
12 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 ) ) ) )
13 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 ) ) ) )
14 fveq1 
 |-  ( c = d -> ( c ` a ) = ( d ` a ) )
15 14 oveq1d 
 |-  ( c = d -> ( ( c ` a ) F b ) = ( ( d ` a ) F b ) )
16 15 mpoeq3dv 
 |-  ( c = d -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) )
17 16 fveq2d 
 |-  ( c = d -> ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) )
18 fveq2 
 |-  ( c = d -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` d ) )
19 18 oveq1d 
 |-  ( c = d -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) )
20 17 19 eqeq12d 
 |-  ( 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 ) ) ) )
21 fveq1 
 |-  ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( c ` a ) = ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) )
22 21 oveq1d 
 |-  ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( c ` a ) F b ) = ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) )
23 22 mpoeq3dv 
 |-  ( 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 ) ) )
24 23 fveq2d 
 |-  ( 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 ) ) ) )
25 fveq2 
 |-  ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) )
26 25 oveq1d 
 |-  ( 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 ) ) )
27 24 26 eqeq12d 
 |-  ( 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 ) ) ) )
28 fveq1 
 |-  ( c = ( 0g ` ( SymGrp ` N ) ) -> ( c ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
29 28 oveq1d 
 |-  ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( c ` a ) F b ) = ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) )
30 29 mpoeq3dv 
 |-  ( 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 ) ) )
31 30 fveq2d 
 |-  ( 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 ) ) ) )
32 fveq2 
 |-  ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) )
33 32 oveq1d 
 |-  ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) .x. ( D ` F ) ) )
34 31 33 eqeq12d 
 |-  ( 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 ) ) ) )
35 fveq1 
 |-  ( c = E -> ( c ` a ) = ( E ` a ) )
36 35 oveq1d 
 |-  ( c = E -> ( ( c ` a ) F b ) = ( ( E ` a ) F b ) )
37 36 mpoeq3dv 
 |-  ( c = E -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) )
38 37 fveq2d 
 |-  ( c = E -> ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( D ` ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) ) )
39 fveq2 
 |-  ( c = E -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) )
40 39 oveq1d 
 |-  ( c = E -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) )
41 38 40 eqeq12d 
 |-  ( 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 ) ) ) )
42 eqid 
 |-  ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
43 eqid 
 |-  ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
44 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
45 8 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> N e. Fin )
46 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
47 46 symggrp 
 |-  ( N e. Fin -> ( SymGrp ` N ) e. Grp )
48 grpmnd 
 |-  ( ( SymGrp ` N ) e. Grp -> ( SymGrp ` N ) e. Mnd )
49 45 47 48 3syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( SymGrp ` N ) e. Mnd )
50 eqid 
 |-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
51 50 46 44 symgtrf 
 |-  ran ( pmTrsp ` N ) C_ ( Base ` ( SymGrp ` N ) )
52 51 a1i 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ran ( pmTrsp ` N ) C_ ( Base ` ( SymGrp ` N ) ) )
53 eqid 
 |-  ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) ) = ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) )
54 50 46 44 53 symggen2 
 |-  ( N e. Fin -> ( ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) ) ` ran ( pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
55 8 54 syl 
 |-  ( ph -> ( ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) ) ` ran ( pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
56 55 eqcomd 
 |-  ( ph -> ( Base ` ( SymGrp ` N ) ) = ( ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) ) ` ran ( pmTrsp ` N ) ) )
57 56 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( Base ` ( SymGrp ` N ) ) = ( ( mrCls ` ( SubMnd ` ( SymGrp ` N ) ) ) ` ran ( pmTrsp ` N ) ) )
58 9 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> R e. Ring )
59 10 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> D : B --> K )
60 simp3 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. B )
61 59 60 ffvelcdmd 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` F ) e. K )
62 3 7 5 ringlidm 
 |-  ( ( R e. Ring /\ ( D ` F ) e. K ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
63 58 61 62 syl2anc 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
64 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
65 9 8 64 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
66 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
67 66 5 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
68 42 67 mhm0 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
69 65 68 syl 
 |-  ( ph -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
70 69 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
71 70 oveq1d 
 |-  ( ( 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 ) ) )
72 46 symgid 
 |-  ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
73 8 72 syl 
 |-  ( ph -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
74 73 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
75 74 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
76 75 fveq1d 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( _I |` N ) ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
77 simp2 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> a e. N )
78 fvresi 
 |-  ( a e. N -> ( ( _I |` N ) ` a ) = a )
79 77 78 syl 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( _I |` N ) ` a ) = a )
80 76 79 eqtr3d 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( 0g ` ( SymGrp ` N ) ) ` a ) = a )
81 80 oveq1d 
 |-  ( ( ( 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 ) )
82 81 mpoeq3dva 
 |-  ( ( 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 ) ) )
83 1 3 2 matbas2i 
 |-  ( F e. B -> F e. ( K ^m ( N X. N ) ) )
84 83 3ad2ant3 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. ( K ^m ( N X. N ) ) )
85 elmapi 
 |-  ( F e. ( K ^m ( N X. N ) ) -> F : ( N X. N ) --> K )
86 ffn 
 |-  ( F : ( N X. N ) --> K -> F Fn ( N X. N ) )
87 84 85 86 3syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F Fn ( N X. N ) )
88 fnov 
 |-  ( F Fn ( N X. N ) <-> F = ( a e. N , b e. N |-> ( a F b ) ) )
89 87 88 sylib 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F = ( a e. N , b e. N |-> ( a F b ) ) )
90 82 89 eqtr4d 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) = F )
91 90 fveq2d 
 |-  ( ( 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 ) )
92 63 71 91 3eqtr4rd 
 |-  ( ( 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 ) ) )
93 simp2 
 |-  ( ( ( 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 ) ) )
94 51 sseli 
 |-  ( e e. ran ( pmTrsp ` N ) -> e e. ( Base ` ( SymGrp ` N ) ) )
95 94 3ad2ant3 
 |-  ( ( ( 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 ) ) )
96 46 44 43 symgov 
 |-  ( ( d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
97 93 95 96 syl2anc 
 |-  ( ( ( 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 ) )
98 97 fveq1d 
 |-  ( ( ( 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 ) )
99 98 3ad2ant1 
 |-  ( ( ( ( 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 ) )
100 46 44 symgbasf1o 
 |-  ( e e. ( Base ` ( SymGrp ` N ) ) -> e : N -1-1-onto-> N )
101 f1of 
 |-  ( e : N -1-1-onto-> N -> e : N --> N )
102 95 100 101 3syl 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> e : N --> N )
103 102 3ad2ant1 
 |-  ( ( ( ( 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 )
104 simp2 
 |-  ( ( ( ( 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 )
105 fvco3 
 |-  ( ( e : N --> N /\ a e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
106 103 104 105 syl2anc 
 |-  ( ( ( ( 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 ) ) )
107 99 106 eqtrd 
 |-  ( ( ( ( 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 ) ) )
108 107 oveq1d 
 |-  ( ( ( ( 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 ) )
109 108 mpoeq3dva 
 |-  ( ( ( 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 ) ) )
110 109 fveq2d 
 |-  ( ( ( 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 ) ) ) )
111 46 44 symgbasf 
 |-  ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N --> N )
112 eqid 
 |-  ( pmTrsp ` N ) = ( pmTrsp ` N )
113 112 50 pmtrrn2 
 |-  ( e e. ran ( pmTrsp ` N ) -> E. c e. N E. f e. N ( c =/= f /\ e = ( ( pmTrsp ` N ) ` { c , f } ) ) )
114 simpll1 
 |-  ( ( ( ( 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 
 |-  ( ( c e. N /\ f e. N /\ c =/= f ) <-> ( ( c e. N /\ f e. N ) /\ c =/= f ) )
116 115 bilanri 
 |-  ( ( ( ( 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 ) )
117 84 85 syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F : ( N X. N ) --> K )
118 117 adantr 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
119 118 ad2antrr 
 |-  ( ( ( ( ( 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 )
120 simpllr 
 |-  ( ( ( ( ( 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 )
121 simprlr 
 |-  ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
122 121 adantr 
 |-  ( ( ( ( ( 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 )
123 120 122 ffvelcdmd 
 |-  ( ( ( ( ( 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 )
124 simpr 
 |-  ( ( ( ( ( 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 )
125 119 123 124 fovcdmd 
 |-  ( ( ( ( ( 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 )
126 simprll 
 |-  ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
127 126 adantr 
 |-  ( ( ( ( ( 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 )
128 120 127 ffvelcdmd 
 |-  ( ( ( ( ( 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 )
129 119 128 124 fovcdmd 
 |-  ( ( ( ( ( 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 )
130 125 129 jca 
 |-  ( ( ( ( ( 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 ) )
131 117 ad2antrr 
 |-  ( ( ( ( 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 )
132 131 3ad2ant1 
 |-  ( ( ( ( ( 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 )
133 simp1lr 
 |-  ( ( ( ( ( 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 )
134 simp2 
 |-  ( ( ( ( ( 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 )
135 133 134 ffvelcdmd 
 |-  ( ( ( ( ( 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 )
136 simp3 
 |-  ( ( ( ( ( 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 )
137 132 135 136 fovcdmd 
 |-  ( ( ( ( ( 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 )
138 1 2 3 4 5 6 7 8 9 10 11 12 13 114 116 130 137 mdetunilem6 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
139 simpl1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
140 fveq2 
 |-  ( a = c -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) )
141 8 adantr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
142 simprll 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
143 simprlr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
144 simprr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
145 112 pmtrprfv 
 |-  ( ( N e. Fin /\ ( c e. N /\ f e. N /\ c =/= f ) ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
146 141 142 143 144 145 syl13anc 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
147 146 adantr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
148 140 147 sylan9eqr 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = f )
149 148 fveq2d 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` f ) )
150 149 oveq1d 
 |-  ( ( ( ( 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 ) )
151 iftrue 
 |-  ( a = c -> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) = ( ( d ` f ) F b ) )
152 151 adantl 
 |-  ( ( ( ( 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 ) )
153 150 152 eqtr4d 
 |-  ( ( ( ( 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 ) ) ) )
154 fveq2 
 |-  ( a = f -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) )
155 prcom 
 |-  { c , f } = { f , c }
156 155 fveq2i 
 |-  ( ( pmTrsp ` N ) ` { c , f } ) = ( ( pmTrsp ` N ) ` { f , c } )
157 156 fveq1i 
 |-  ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( ( pmTrsp ` N ) ` { f , c } ) ` f )
158 8 ad2antrr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
159 simplrl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
160 159 simprd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
161 159 simpld 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
162 simplrr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
163 162 necomd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
164 112 pmtrprfv 
 |-  ( ( N e. Fin /\ ( f e. N /\ c e. N /\ f =/= c ) ) -> ( ( ( pmTrsp ` N ) ` { f , c } ) ` f ) = c )
165 158 160 161 163 164 syl13anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { f , c } ) ` f ) = c )
166 157 165 eqtrid 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) = c )
167 154 166 sylan9eqr 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = c )
168 167 fveq2d 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` c ) )
169 168 oveq1d 
 |-  ( ( ( ( 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 ) )
170 iftrue 
 |-  ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
171 170 adantl 
 |-  ( ( ( ( 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 ) )
172 169 171 eqtr4d 
 |-  ( ( ( ( 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 ) ) )
173 172 adantlr 
 |-  ( ( ( ( ( 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 ) ) )
174 vex 
 |-  a e. _V
175 174 elpr 
 |-  ( a e. { c , f } <-> ( a = c \/ a = f ) )
176 175 notbii 
 |-  ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
177 ioran 
 |-  ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
178 176 177 sylbbr 
 |-  ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
179 178 adantll 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
180 prssi 
 |-  ( ( c e. N /\ f e. N ) -> { c , f } C_ N )
181 159 180 syl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } C_ N )
182 pr2ne 
 |-  ( ( c e. N /\ f e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
183 159 182 syl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
184 162 183 mpbird 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
185 112 pmtrmvd 
 |-  ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
186 158 181 184 185 syl3anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
187 186 eleq2d 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) <-> a e. { c , f } ) )
188 187 notbid 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( -. a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) <-> -. a e. { c , f } ) )
189 188 ad2antrr 
 |-  ( ( ( ( ( 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 } ) )
190 179 189 mpbird 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) )
191 112 pmtrf 
 |-  ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( ( pmTrsp ` N ) ` { c , f } ) : N --> N )
192 158 181 184 191 syl3anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( pmTrsp ` N ) ` { c , f } ) : N --> N )
193 192 ffnd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( pmTrsp ` N ) ` { c , f } ) Fn N )
194 simpr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
195 fnelnfp 
 |-  ( ( ( ( pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) <-> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) =/= a ) )
196 195 necon2bbid 
 |-  ( ( ( ( pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
197 193 194 196 syl2anc 
 |-  ( ( ( 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 ) ) )
198 197 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
199 190 198 mpbird 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = a )
200 199 fveq2d 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` a ) )
201 200 oveq1d 
 |-  ( ( ( ( ( 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 ) )
202 iffalse 
 |-  ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
203 202 adantl 
 |-  ( ( ( ( ( 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 ) )
204 201 203 eqtr4d 
 |-  ( ( ( ( ( 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 ) ) )
205 173 204 pm2.61dan 
 |-  ( ( ( ( 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 ) ) )
206 iffalse 
 |-  ( -. 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 ) ) )
207 206 adantl 
 |-  ( ( ( ( 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 ) ) )
208 205 207 eqtr4d 
 |-  ( ( ( ( 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 ) ) ) )
209 153 208 pm2.61dan 
 |-  ( ( ( 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 ) ) ) )
210 209 3adant3 
 |-  ( ( ( 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 ) ) ) )
211 210 mpoeq3dva 
 |-  ( ( 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 ) ) ) ) )
212 139 211 sylan 
 |-  ( ( ( ( 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 ) ) ) ) )
213 212 fveq2d 
 |-  ( ( ( ( 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 ) ) ) ) ) )
214 fveq2 
 |-  ( a = c -> ( d ` a ) = ( d ` c ) )
215 214 oveq1d 
 |-  ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
216 iftrue 
 |-  ( a = c -> if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) = ( ( d ` c ) F b ) )
217 215 216 eqtr4d 
 |-  ( a = c -> ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
218 fveq2 
 |-  ( a = f -> ( d ` a ) = ( d ` f ) )
219 218 oveq1d 
 |-  ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
220 iftrue 
 |-  ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
221 219 220 eqtr4d 
 |-  ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
222 221 adantl 
 |-  ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
223 iffalse 
 |-  ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
224 223 eqcomd 
 |-  ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
225 224 adantl 
 |-  ( ( -. a = c /\ -. a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
226 222 225 pm2.61dan 
 |-  ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
227 iffalse 
 |-  ( -. 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 ) ) )
228 226 227 eqtr4d 
 |-  ( -. a = c -> ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
229 217 228 pm2.61i 
 |-  ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
230 229 a1i 
 |-  ( ( 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 ) ) ) )
231 230 mpoeq3ia 
 |-  ( 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 ) ) ) )
232 231 fveq2i 
 |-  ( 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 ) ) ) ) )
233 232 fveq2i 
 |-  ( ( 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 ) ) ) ) ) )
234 233 a1i 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
235 138 213 234 3eqtr4d 
 |-  ( ( ( ( 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 ) ) ) ) )
236 fveq1 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) )
237 236 fveq2d 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) )
238 237 oveq1d 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
239 238 mpoeq3dv 
 |-  ( 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 ) ) )
240 239 fveqeq2d 
 |-  ( 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 ) ) ) ) ) )
241 235 240 syl5ibrcom 
 |-  ( ( ( ( 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 ) ) ) ) ) )
242 241 expr 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
243 242 impd 
 |-  ( ( ( ( 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 ) ) ) ) ) )
244 243 rexlimdvva 
 |-  ( ( ( 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 ) ) ) ) ) )
245 113 244 syl5 
 |-  ( ( ( 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 ) ) ) ) ) )
246 245 3impia 
 |-  ( ( ( 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 ) ) ) ) )
247 111 246 syl3an2 
 |-  ( ( ( 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 ) ) ) ) )
248 110 247 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
249 248 adantr 
 |-  ( ( ( ( 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 ) ) ) ) )
250 fveq2 
 |-  ( ( 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 ) ) ) )
251 250 adantl 
 |-  ( ( ( ( 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 ) ) ) )
252 eqid 
 |-  ( invg ` R ) = ( invg ` R )
253 58 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> R e. Ring )
254 65 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
255 254 3ad2ant1 
 |-  ( ( ( 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 ) ) )
256 66 3 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
257 44 256 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
258 255 257 syl 
 |-  ( ( ( 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 )
259 258 93 ffvelcdmd 
 |-  ( ( ( 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 )
260 59 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> D : B --> K )
261 simp13 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> F e. B )
262 260 261 ffvelcdmd 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> ( D ` F ) e. K )
263 3 7 252 253 259 262 ringmneg1 
 |-  ( ( ( 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 ) ) ) )
264 66 7 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
265 44 43 264 mhmlin 
 |-  ( ( ( ( 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 ) ) )
266 255 93 95 265 syl3anc 
 |-  ( ( ( 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 ) ) )
267 45 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> N e. Fin )
268 simp3 
 |-  ( ( ( 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 ) )
269 46 44 50 pmtrodpm 
 |-  ( ( N e. Fin /\ e e. ran ( pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ ( pmEven ` N ) ) )
270 267 268 269 syl2anc 
 |-  ( ( ( 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 ) ) )
271 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
272 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
273 271 272 5 44 252 zrhpsgnodpm 
 |-  ( ( R e. Ring /\ N e. Fin /\ e e. ( ( Base ` ( SymGrp ` N ) ) \ ( pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
274 253 267 270 273 syl3anc 
 |-  ( ( ( 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. ) )
275 274 oveq2d 
 |-  ( ( ( 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. ) ) )
276 3 7 5 252 253 259 ringnegr 
 |-  ( ( ( 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 ) ) )
277 266 275 276 3eqtrrd 
 |-  ( ( ( 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 ) ) )
278 277 oveq1d 
 |-  ( ( ( 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 ) ) )
279 263 278 eqtr3d 
 |-  ( ( ( 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 ) ) )
280 279 adantr 
 |-  ( ( ( ( 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 ) ) )
281 249 251 280 3eqtrd 
 |-  ( ( ( ( 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 ) ) )
282 simp2 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
283 46 44 elsymgbas 
 |-  ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
284 45 283 syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
285 282 284 mpbird 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E e. ( Base ` ( SymGrp ` N ) ) )
286 20 27 34 41 42 43 44 49 52 57 92 281 285 mndind 
 |-  ( ( 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 ) ) )