This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimpri 
 |-  ( ( ( c e. N /\ f e. N ) /\ c =/= f ) -> ( c e. N /\ f e. N /\ c =/= f ) )
117 116 adantl 
 |-  ( ( ( ( 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 ) )
118 84 85 syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F : ( N X. N ) --> K )
119 118 adantr 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
120 119 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 )
121 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 )
122 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 )
123 122 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 )
124 121 123 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 )
125 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 )
126 120 124 125 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 )
127 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 )
128 127 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 )
129 121 128 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 )
130 120 129 125 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 )
131 126 130 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 ) )
132 118 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 )
133 132 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 )
134 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 )
135 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 )
136 134 135 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 )
137 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 )
138 133 136 137 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 )
139 1 2 3 4 5 6 7 8 9 10 11 12 13 114 117 131 138 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 ) ) ) ) ) ) )
140 simpl1 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
141 fveq2 
 |-  ( a = c -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) )
142 8 adantr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
143 simprll 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
144 simprlr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
145 simprr 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
146 112 pmtrprfv 
 |-  ( ( N e. Fin /\ ( c e. N /\ f e. N /\ c =/= f ) ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
147 142 143 144 145 146 syl13anc 
 |-  ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
148 147 adantr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` c ) = f )
149 141 148 sylan9eqr 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = f )
150 149 fveq2d 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` f ) )
151 150 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 ) )
152 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 ) )
153 152 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 ) )
154 151 153 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 ) ) ) )
155 fveq2 
 |-  ( a = f -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) )
156 prcom 
 |-  { c , f } = { f , c }
157 156 fveq2i 
 |-  ( ( pmTrsp ` N ) ` { c , f } ) = ( ( pmTrsp ` N ) ` { f , c } )
158 157 fveq1i 
 |-  ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( ( pmTrsp ` N ) ` { f , c } ) ` f )
159 8 ad2antrr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
160 simplrl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
161 160 simprd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
162 160 simpld 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
163 simplrr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
164 163 necomd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
165 112 pmtrprfv 
 |-  ( ( N e. Fin /\ ( f e. N /\ c e. N /\ f =/= c ) ) -> ( ( ( pmTrsp ` N ) ` { f , c } ) ` f ) = c )
166 159 161 162 164 165 syl13anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { f , c } ) ` f ) = c )
167 158 166 eqtrid 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` f ) = c )
168 155 167 sylan9eqr 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = c )
169 168 fveq2d 
 |-  ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` c ) )
170 169 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 ) )
171 iftrue 
 |-  ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
172 171 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 ) )
173 170 172 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 ) ) )
174 173 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 ) ) )
175 vex 
 |-  a e. _V
176 175 elpr 
 |-  ( a e. { c , f } <-> ( a = c \/ a = f ) )
177 176 notbii 
 |-  ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
178 ioran 
 |-  ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
179 177 178 sylbbr 
 |-  ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
180 179 adantll 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
181 prssi 
 |-  ( ( c e. N /\ f e. N ) -> { c , f } C_ N )
182 160 181 syl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } C_ N )
183 pr2ne 
 |-  ( ( c e. N /\ f e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
184 160 183 syl 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
185 163 184 mpbird 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
186 112 pmtrmvd 
 |-  ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
187 159 182 185 186 syl3anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
188 187 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 } ) )
189 188 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 } ) )
190 189 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 } ) )
191 180 190 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 ) )
192 112 pmtrf 
 |-  ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( ( pmTrsp ` N ) ` { c , f } ) : N --> N )
193 159 182 185 192 syl3anc 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( pmTrsp ` N ) ` { c , f } ) : N --> N )
194 193 ffnd 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( pmTrsp ` N ) ` { c , f } ) Fn N )
195 simpr 
 |-  ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
196 fnelnfp 
 |-  ( ( ( ( pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) <-> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) =/= a ) )
197 196 necon2bbid 
 |-  ( ( ( ( pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( ( pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
198 194 195 197 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 ) ) )
199 198 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 ) ) )
200 191 199 mpbird 
 |-  ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) = a )
201 200 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 ) )
202 201 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 ) )
203 iffalse 
 |-  ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
204 203 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 ) )
205 202 204 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 ) ) )
206 174 205 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 ) ) )
207 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 ) ) )
208 207 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 ) ) )
209 206 208 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 ) ) ) )
210 154 209 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 ) ) ) )
211 210 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 ) ) ) )
212 211 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 ) ) ) ) )
213 140 212 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 ) ) ) ) )
214 213 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 ) ) ) ) ) )
215 fveq2 
 |-  ( a = c -> ( d ` a ) = ( d ` c ) )
216 215 oveq1d 
 |-  ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
217 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 ) )
218 216 217 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 ) ) ) )
219 fveq2 
 |-  ( a = f -> ( d ` a ) = ( d ` f ) )
220 219 oveq1d 
 |-  ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
221 iftrue 
 |-  ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
222 220 221 eqtr4d 
 |-  ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
223 222 adantl 
 |-  ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
224 iffalse 
 |-  ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
225 224 eqcomd 
 |-  ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
226 225 adantl 
 |-  ( ( -. a = c /\ -. a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
227 223 226 pm2.61dan 
 |-  ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
228 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 ) ) )
229 227 228 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 ) ) ) )
230 218 229 pm2.61i 
 |-  ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
231 230 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 ) ) ) )
232 231 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 ) ) ) )
233 232 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 ) ) ) ) )
234 233 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 ) ) ) ) ) )
235 234 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 ) ) ) ) ) ) )
236 139 214 235 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 ) ) ) ) )
237 fveq1 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) )
238 237 fveq2d 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) )
239 238 oveq1d 
 |-  ( e = ( ( pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( ( pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
240 239 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 ) ) )
241 240 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 ) ) ) ) ) )
242 236 241 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 ) ) ) ) ) )
243 242 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 ) ) ) ) ) ) )
244 243 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 ) ) ) ) ) )
245 244 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 ) ) ) ) ) )
246 113 245 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 ) ) ) ) ) )
247 246 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 ) ) ) ) )
248 111 247 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 ) ) ) ) )
249 110 248 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 ) ) ) ) )
250 249 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 ) ) ) ) )
251 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 ) ) ) )
252 251 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 ) ) ) )
253 eqid 
 |-  ( invg ` R ) = ( invg ` R )
254 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 )
255 65 3ad2ant1 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
256 255 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 ) ) )
257 66 3 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
258 44 257 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
259 256 258 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 )
260 259 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 )
261 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 )
262 simp13 
 |-  ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran ( pmTrsp ` N ) ) -> F e. B )
263 261 262 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 )
264 3 7 253 254 260 263 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 ) ) ) )
265 66 7 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
266 44 43 265 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 ) ) )
267 256 93 95 266 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 ) ) )
268 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 )
269 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 ) )
270 46 44 50 pmtrodpm 
 |-  ( ( N e. Fin /\ e e. ran ( pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ ( pmEven ` N ) ) )
271 268 269 270 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 ) ) )
272 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
273 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
274 272 273 5 44 253 zrhpsgnodpm 
 |-  ( ( R e. Ring /\ N e. Fin /\ e e. ( ( Base ` ( SymGrp ` N ) ) \ ( pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
275 254 268 271 274 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. ) )
276 275 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. ) ) )
277 3 7 5 253 254 260 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 ) ) )
278 267 276 277 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 ) ) )
279 278 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 ) ) )
280 264 279 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 ) ) )
281 280 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 ) ) )
282 250 252 281 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 ) ) )
283 simp2 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
284 46 44 elsymgbas 
 |-  ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
285 45 284 syl 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
286 283 285 mpbird 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E e. ( Base ` ( SymGrp ` N ) ) )
287 20 27 34 41 42 43 44 49 52 57 92 282 286 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 ) ) )