Theorem mdetunilem7 19720

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

Hypotheses

Ref	Expression
mdetuni.a	|- A = ( N Mat R )
mdetuni.b	|- B = ( Base ` A )
mdetuni.k	|- K = ( Base ` R )
mdetuni.0g	|- .0. = ( 0g ` R )
mdetuni.1r	|- .1. = ( 1r ` R )
mdetuni.pg	|- .+ = ( +g ` R )
mdetuni.tg	|- .x. = ( .r ` R )
mdetuni.n	|- ( ph -> N e. Fin )
mdetuni.r	|- ( ph -> R e. Ring )
mdetuni.ff	|- ( ph -> D : B --> K )
mdetuni.al	|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
mdetuni.li	|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
mdetuni.sc	|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )

Assertion

Ref	Expression
mdetunilem7	|- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) )

Distinct variable groups:   ph, x, y, z, w, a, b   x, B, y, z, w, a, b   x, K, y, z, w, a, b   x, N, y, z, w, a, b   x, D, y, z, w, a, b   x, .x. , y, z, w   .+ , a, b, x, y, z, w   .0. , a, b, x, y, z, w   .1. , a, b, x, y, z, w   x, R, y, z, w   A, a, b, x, y, z, w   x, E, y, z, w   x, F, y, z, w   E, a, b   F, a, b

Allowed substitution hints:   R( a, b)   .x. ( a, b)

Proof of Theorem mdetunilem7

Dummy variables c d e f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq1 5878	. . . . . 6 |- ( c = d -> ( c ` a ) = ( d ` a ) )
2	1	oveq1d 6323	. . . . 5 |- ( c = d -> ( ( c ` a ) F b ) = ( ( d ` a ) F b ) )
3	2	mpt2eq3dv 6376	. . . 4 |- ( c = d -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) )
4	3	fveq2d 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 ) )
6	5	oveq1d 6323	. . 3 |- ( c = d -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) )
7	4, 6	eqeq12d 2486	. 2 |- ( c = d -> ( ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) <-> ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) )
8		fveq1 5878	. . . . . 6 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( c ` a ) = ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) )
9	8	oveq1d 6323	. . . . 5 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( c ` a ) F b ) = ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) )
10	9	mpt2eq3dv 6376	. . . 4 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) )
11	10	fveq2d 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 ) ) )
13	12	oveq1d 6323	. . 3 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
14	11, 13	eqeq12d 2486	. 2 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) <-> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) ) )
15		fveq1 5878	. . . . . 6 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( c ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
16	15	oveq1d 6323	. . . . 5 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( c ` a ) F b ) = ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) )
17	16	mpt2eq3dv 6376	. . . 4 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) )
18	17	fveq2d 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 ) ) ) )
20	19	oveq1d 6323	. . 3 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) .x. ( D ` F ) ) )
21	18, 20	eqeq12d 2486	. 2 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) <-> ( D ` ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) .x. ( D ` F ) ) ) )
22		fveq1 5878	. . . . . 6 |- ( c = E -> ( c ` a ) = ( E ` a ) )
23	22	oveq1d 6323	. . . . 5 |- ( c = E -> ( ( c ` a ) F b ) = ( ( E ` a ) F b ) )
24	23	mpt2eq3dv 6376	. . . 4 |- ( c = E -> ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) )
25	24	fveq2d 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 ) )
27	26	oveq1d 6323	. . 3 |- ( c = E -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) )
28	25, 27	eqeq12d 2486	. 2 |- ( c = E -> ( ( D ` ( a e. N , b e. N |-> ( ( c ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) .x. ( D ` F ) ) <-> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) ) )
29		eqid 2471	. 2 |- ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
30		eqid 2471	. 2 |- ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
31		eqid 2471	. 2 |- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
32		mdetuni.n	. . . 4 |- ( ph -> N e. Fin )
33	32	3ad2ant1 1051	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> N e. Fin )
34		eqid 2471	. . . 4 |- ( SymGrp ` N ) = ( SymGrp ` N )
35	34	symggrp 17119	. . 3 |- ( N e. Fin -> ( SymGrp ` N ) e. Grp )
36		grpmnd 16756	. . 3 |- ( ( SymGrp ` N ) e. Grp -> ( SymGrp ` N ) e. Mnd )
37	33, 35, 36	3syl 18	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( SymGrp ` N ) e. Mnd )
38		eqid 2471	. . . 4 |- ran (pmTrsp ` N ) = ran (pmTrsp ` N )
39	38, 34, 31	symgtrf 17188	. . 3 |- ran (pmTrsp ` N ) C_ ( Base ` ( SymGrp ` N ) )
40	39	a1i 11	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ran (pmTrsp ` N ) C_ ( Base ` ( SymGrp ` N ) ) )
41		eqid 2471	. . . . . 6 |- (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) = (mrCls ` (SubMnd ` ( SymGrp ` N ) ) )
42	38, 34, 31, 41	symggen2 17190	. . . . 5 |- ( N e. Fin -> ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
43	32, 42	syl 17	. . . 4 |- ( ph -> ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
44	43	eqcomd 2477	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) = ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) )
45	44	3ad2ant1 1051	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( Base ` ( SymGrp ` N ) ) = ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) )
46		mdetuni.r	. . . . 5 |- ( ph -> R e. Ring )
47	46	3ad2ant1 1051	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> R e. Ring )
48		mdetuni.ff	. . . . . 6 |- ( ph -> D : B --> K )
49	48	3ad2ant1 1051	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> D : B --> K )
50		simp3 1032	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. B )
51	49, 50	ffvelrnd 6038	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` F ) e. K )
52		mdetuni.k	. . . . 5 |- K = ( Base ` R )
53		mdetuni.tg	. . . . 5 |- .x. = ( .r ` R )
54		mdetuni.1r	. . . . 5 |- .1. = ( 1r ` R )
55	52, 53, 54	ringlidm 17882	. . . 4 |- ( ( R e. Ring /\ ( D ` F ) e. K ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
56	47, 51, 55	syl2anc 673	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
57		zrhpsgnmhm 19229	. . . . . . 7 |- ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
58	46, 32, 57	syl2anc 673	. . . . . 6 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
59		eqid 2471	. . . . . . . 8 |- (mulGrp ` R ) = (mulGrp ` R )
60	59, 54	ringidval 17815	. . . . . . 7 |- .1. = ( 0g ` (mulGrp ` R ) )
61	29, 60	mhm0 16668	. . . . . 6 |- ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
62	58, 61	syl 17	. . . . 5 |- ( ph -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
63	62	3ad2ant1 1051	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
64	63	oveq1d 6323	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) .x. ( D ` F ) ) = ( .1. .x. ( D ` F ) ) )
65	34	symgid 17120	. . . . . . . . . . . 12 |- ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
66	32, 65	syl 17	. . . . . . . . . . 11 |- ( ph -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
67	66	3ad2ant1 1051	. . . . . . . . . 10 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
68	67	3ad2ant1 1051	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
69	68	fveq1d 5881	. . . . . . . 8 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( _I |` N ) ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
70		simp2 1031	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> a e. N )
71		fvresi 6106	. . . . . . . . 9 |- ( a e. N -> ( ( _I |` N ) ` a ) = a )
72	70, 71	syl 17	. . . . . . . 8 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( _I |` N ) ` a ) = a )
73	69, 72	eqtr3d 2507	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( 0g ` ( SymGrp ` N ) ) ` a ) = a )
74	73	oveq1d 6323	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) = ( a F b ) )
75	74	mpt2eq3dva 6374	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) = ( a e. N , b e. N |-> ( a F b ) ) )
76		mdetuni.a	. . . . . . . . 9 |- A = ( N Mat R )
77		mdetuni.b	. . . . . . . . 9 |- B = ( Base ` A )
78	76, 52, 77	matbas2i 19524	. . . . . . . 8 |- ( F e. B -> F e. ( K ^m ( N X. N ) ) )
79	78	3ad2ant3 1053	. . . . . . 7 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. ( K ^m ( N X. N ) ) )
80		elmapi 7511	. . . . . . 7 |- ( F e. ( K ^m ( N X. N ) ) -> F : ( N X. N ) --> K )
81		ffn 5739	. . . . . . 7 |- ( F : ( N X. N ) --> K -> F Fn ( N X. N ) )
82	79, 80, 81	3syl 18	. . . . . 6 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F Fn ( N X. N ) )
83		fnov 6423	. . . . . 6 |- ( F Fn ( N X. N ) <-> F = ( a e. N , b e. N |-> ( a F b ) ) )
84	82, 83	sylib 201	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F = ( a e. N , b e. N |-> ( a F b ) ) )
85	75, 84	eqtr4d 2508	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) = F )
86	85	fveq2d 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 ) )
87	56, 64, 86	3eqtr4rd 2516	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` ( a e. N , b e. N |-> ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) .x. ( D ` F ) ) )
88		simp2 1031	. . . . . . . . . . . 12 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> d e. ( Base ` ( SymGrp ` N ) ) )
89	39	sseli 3414	. . . . . . . . . . . . 13 |- ( e e. ran (pmTrsp ` N ) -> e e. ( Base ` ( SymGrp ` N ) ) )
90	89	3ad2ant3 1053	. . . . . . . . . . . 12 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> e e. ( Base ` ( SymGrp ` N ) ) )
91	34, 31, 30	symgov 17109	. . . . . . . . . . . 12 |- ( ( d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
92	88, 90, 91	syl2anc 673	. . . . . . . . . . 11 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
93	92	fveq1d 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 ) )
94	93	3ad2ant1 1051	. . . . . . . . 9 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) = ( ( d o. e ) ` a ) )
95	34, 31	symgbasf1o 17102	. . . . . . . . . . . 12 |- ( e e. ( Base ` ( SymGrp ` N ) ) -> e : N -1-1-onto-> N )
96		f1of 5828	. . . . . . . . . . . 12 |- ( e : N -1-1-onto-> N -> e : N --> N )
97	90, 95, 96	3syl 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 )
98	97	3ad2ant1 1051	. . . . . . . . . 10 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> e : N --> N )
99		simp2 1031	. . . . . . . . . 10 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> a e. N )
100		fvco3 5957	. . . . . . . . . 10 |- ( ( e : N --> N /\ a e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
101	98, 99, 100	syl2anc 673	. . . . . . . . 9 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
102	94, 101	eqtrd 2505	. . . . . . . 8 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) = ( d ` ( e ` a ) ) )
103	102	oveq1d 6323	. . . . . . 7 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ a e. N /\ b e. N ) -> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) = ( ( d ` ( e ` a ) ) F b ) )
104	103	mpt2eq3dva 6374	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) = ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) )
105	104	fveq2d 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 ) ) ) )
106	34, 31	symgbasf 17103	. . . . . 6 |- ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N --> N )
107		eqid 2471	. . . . . . . . 9 |- (pmTrsp ` N ) = (pmTrsp ` N )
108	107, 38	pmtrrn2 17179	. . . . . . . 8 |- ( e e. ran (pmTrsp ` N ) -> E. c e. N E. f e. N ( c =/= f /\ e = ( (pmTrsp ` N ) ` { c , f } ) ) )
109		mdetuni.0g	. . . . . . . . . . . . . 14 |- .0. = ( 0g ` R )
110		mdetuni.pg	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
111		mdetuni.al	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
112		mdetuni.li	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
113		mdetuni.sc	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
114		simpll1 1069	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ph )
115		df-3an 1009	. . . . . . . . . . . . . . . 16 |- ( ( c e. N /\ f e. N /\ c =/= f ) <-> ( ( c e. N /\ f e. N ) /\ c =/= f ) )
116	115	biimpri 211	. . . . . . . . . . . . . . 15 |- ( ( ( c e. N /\ f e. N ) /\ c =/= f ) -> ( c e. N /\ f e. N /\ c =/= f ) )
117	116	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( c e. N /\ f e. N /\ c =/= f ) )
118	79, 80	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F : ( N X. N ) --> K )
119	118	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
120	119	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> F : ( N X. N ) --> K )
121		simpllr 777	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> d : N --> N )
122		simprlr 781	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
123	122	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> f e. N )
124	121, 123	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> ( d ` f ) e. N )
125		simpr 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> b e. N )
126	120, 124, 125	fovrnd 6460	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> ( ( d ` f ) F b ) e. K )
127		simprll 780	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
128	127	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> c e. N )
129	121, 128	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> ( d ` c ) e. N )
130	120, 129, 125	fovrnd 6460	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> ( ( d ` c ) F b ) e. K )
131	126, 130	jca 541	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ b e. N ) -> ( ( ( d ` f ) F b ) e. K /\ ( ( d ` c ) F b ) e. K ) )
132	118	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> F : ( N X. N ) --> K )
133	132	3ad2ant1 1051	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> F : ( N X. N ) --> K )
134		simp1lr 1094	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> d : N --> N )
135		simp2 1031	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> a e. N )
136	134, 135	ffvelrnd 6038	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> ( d ` a ) e. N )
137		simp3 1032	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> b e. N )
138	133, 136, 137	fovrnd 6460	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> ( ( d ` a ) F b ) e. K )
139	76, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138	mdetunilem6 19719	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) ) ) ) )
140		simpl1 1033	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
141		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = c -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) )
142	32	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
143		simprll 780	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
144		simprlr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
145		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
146	107	pmtrprfv 17172	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( N e. Fin /\ ( c e. N /\ f e. N /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
147	142, 143, 144, 145, 146	syl13anc 1294	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
148	147	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
149	141, 148	sylan9eqr 2527	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = f )
150	149	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 6323	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = ( ( d ` f ) F b ) )
152		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) = ( ( d ` f ) F b ) )
153	152	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) = ( ( d ` f ) F b ) )
154	151, 153	eqtr4d 2508	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) )
155		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = f -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) )
156		prcom 4041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { c , f } = { f , c }
157	156	fveq2i 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( (pmTrsp ` N ) ` { c , f } ) = ( (pmTrsp ` N ) ` { f , c } )
158	157	fveq1i 5880	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( (pmTrsp ` N ) ` { f , c } ) ` f )
159	32	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
160		simplrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
161	160	simprd 470	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
162	160	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
163		simplrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
164	163	necomd 2698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
165	107	pmtrprfv 17172	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. Fin /\ ( f e. N /\ c e. N /\ f =/= c ) ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
166	159, 161, 162, 164, 165	syl13anc 1294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
167	158, 166	syl5eq 2517	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = c )
168	155, 167	sylan9eqr 2527	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = c )
169	168	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 6323	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = ( ( d ` c ) F b ) )
171		iftrue 3878	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
172	171	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
173	170, 172	eqtr4d 2508	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
174	173	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
175		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- a e. _V
176	175	elpr 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( a e. { c , f } <-> ( a = c \/ a = f ) )
177	176	notbii 303	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
178		ioran 498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
179	177, 178	sylbbr 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
180	179	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
181		prssi 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( c e. N /\ f e. N ) -> { c , f } C_ N )
182	160, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } C_ N )
183		pr2ne 8454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( c e. N /\ f e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
184	160, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
185	163, 184	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
186	107	pmtrmvd 17175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
187	159, 182, 185, 186	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
188	187	eleq2d 2534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> a e. { c , f } ) )
189	188	notbid 301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> -. a e. { c , f } ) )
190	189	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> -. a e. { c , f } ) )
191	180, 190	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) )
192	107	pmtrf 17174	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
193	159, 182, 185, 192	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
194		ffn 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( (pmTrsp ` N ) ` { c , f } ) : N --> N -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
195	193, 194	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
196		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
197		fnelnfp 6110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) =/= a ) )
198	197	necon2bbid 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
199	195, 196, 198	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
200	199	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
201	191, 200	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a )
202	201	fveq2d 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 ) )
203	202	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = ( ( d ` a ) F b ) )
204		iffalse 3881	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
205	204	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
206	203, 205	eqtr4d 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
207	174, 206	pm2.61dan 808	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
208		iffalse 3881	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
209	208	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) -> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
210	207, 209	eqtr4d 2508	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) )
211	154, 210	pm2.61dan 808	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) )
212	211	3adant3 1050	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N /\ b e. N ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) )
213	212	mpt2eq3dva 6374	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) = ( a e. N , b e. N |-> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) ) )
214	140, 213	sylan 479	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) = ( a e. N , b e. N |-> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) ) )
215	214	fveq2d 5883	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) ) ) )
216		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = c -> ( d ` a ) = ( d ` c ) )
217	216	oveq1d 6323	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
218		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) = ( ( d ` c ) F b ) )
219	217, 218	eqtr4d 2508	. . . . . . . . . . . . . . . . . . 19 |- ( a = c -> ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
220		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = f -> ( d ` a ) = ( d ` f ) )
221	220	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
222		iftrue 3878	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
223	221, 222	eqtr4d 2508	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
224	223	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
225		iffalse 3881	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
226	225	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
227	226	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ -. a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
228	224, 227	pm2.61dan 808	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
229		iffalse 3881	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
230	228, 229	eqtr4d 2508	. . . . . . . . . . . . . . . . . . 19 |- ( -. a = c -> ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
231	219, 230	pm2.61i 169	. . . . . . . . . . . . . . . . . 18 |- ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
232	231	a1i 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 ) ) ) )
233	232	mpt2eq3ia 6375	. . . . . . . . . . . . . . . 16 |- ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) = ( a e. N , b e. N |-> if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
234	233	fveq2i 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 ) ) ) ) )
235	234	fveq2i 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 ) ) ) ) ) )
236	235	a1i 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 ) ) ) ) ) ) )
237	139, 215, 236	3eqtr4d 2515	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
238		fveq1 5878	. . . . . . . . . . . . . . . . 17 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) )
239	238	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) )
240	239	oveq1d 6323	. . . . . . . . . . . . . . 15 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
241	240	mpt2eq3dv 6376	. . . . . . . . . . . . . 14 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) = ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) )
242	241	fveq2d 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 ) ) ) )
243	242	eqeq1d 2473	. . . . . . . . . . . 12 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) <-> ( D ` ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) )
244	237, 243	syl5ibrcom 230	. . . . . . . . . . 11 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) )
245	244	expr 626	. . . . . . . . . 10 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( c e. N /\ f e. N ) ) -> ( c =/= f -> ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) ) )
246	245	impd 438	. . . . . . . . 9 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( c e. N /\ f e. N ) ) -> ( ( c =/= f /\ e = ( (pmTrsp ` N ) ` { c , f } ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) )
247	246	rexlimdvva 2878	. . . . . . . 8 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ( E. c e. N E. f e. N ( c =/= f /\ e = ( (pmTrsp ` N ) ` { c , f } ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) )
248	108, 247	syl5 32	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ( e e. ran (pmTrsp ` N ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) ) )
249	248	3impia 1228	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N /\ e e. ran (pmTrsp ` N ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
250	106, 249	syl3an2 1326	. . . . 5 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( e ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
251	105, 250	eqtrd 2505	. . . 4 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
252	251	adantr 472	. . 3 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
253		fveq2 5879	. . . 4 |- ( ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) -> ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) = ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) )
254	253	adantl 473	. . 3 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) = ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) )
255		eqid 2471	. . . . . 6 |- ( invg ` R ) = ( invg ` R )
256	47	3ad2ant1 1051	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> R e. Ring )
257	58	3ad2ant1 1051	. . . . . . . . 9 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
258	257	3ad2ant1 1051	. . . . . . . 8 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
259	59, 52	mgpbas 17807	. . . . . . . . 9 |- K = ( Base ` (mulGrp ` R ) )
260	31, 259	mhmf 16665	. . . . . . . 8 |- ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
261	258, 260	syl 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 )
262	261, 88	ffvelrnd 6038	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) e. K )
263	49	3ad2ant1 1051	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> D : B --> K )
264		simp13 1062	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> F e. B )
265	263, 264	ffvelrnd 6038	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( D ` F ) e. K )
266	52, 53, 255, 256, 262, 265	ringmneg1 17902	. . . . 5 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( invg ` R ) ` ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) ) .x. ( D ` F ) ) = ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) )
267	59, 53	mgpplusg 17805	. . . . . . . . 9 |- .x. = ( +g ` (mulGrp ` R ) )
268	31, 30, 267	mhmlin 16667	. . . . . . . 8 |- ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) ) )
269	258, 88, 90, 268	syl3anc 1292	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) ) )
270	33	3ad2ant1 1051	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> N e. Fin )
271		simp3 1032	. . . . . . . . . 10 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> e e. ran (pmTrsp ` N ) )
272	34, 31, 38	pmtrodpm 19242	. . . . . . . . . 10 |- ( ( N e. Fin /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
273	270, 271, 272	syl2anc 673	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
274		eqid 2471	. . . . . . . . . 10 |- ( ZRHom ` R ) = ( ZRHom ` R )
275		eqid 2471	. . . . . . . . . 10 |- (pmSgn ` N ) = (pmSgn ` N )
276	274, 275, 54, 31, 255	zrhpsgnodpm 19237	. . . . . . . . 9 |- ( ( R e. Ring /\ N e. Fin /\ e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
277	256, 270, 273, 276	syl3anc 1292	. . . . . . . 8 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
278	277	oveq2d 6324	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( ( invg ` R ) ` .1. ) ) )
279	52, 53, 54, 255, 256, 262	rngnegr 17901	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( ( invg ` R ) ` .1. ) ) = ( ( invg ` R ) ` ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) ) )
280	269, 278, 279	3eqtrrd 2510	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( invg ` R ) ` ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) )
281	280	oveq1d 6323	. . . . 5 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( ( invg ` R ) ` ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) ) .x. ( D ` F ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
282	266, 281	eqtr3d 2507	. . . 4 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
283	282	adantr 472	. . 3 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
284	252, 254, 283	3eqtrd 2509	. 2 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
285		simp2 1031	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
286	34, 31	elsymgbas 17101	. . . 4 |- ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
287	33, 286	syl 17	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
288	285, 287	mpbird 240	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E e. ( Base ` ( SymGrp ` N ) ) )
289	7, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 284, 288	mrcmndind 16691	1 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   \ cdif 3387   C_ wss 3390   ifcif 3872   {csn 3959   {cpr 3961   class class class wbr 4395   _I cid 4749   X. cxp 4837   dom cdm 4839   ran crn 4840   |` cres 4841   o. ccom 4843   Fn wfn 5584   -->wf 5585   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308   |-> cmpt2 6310   oFcof 6548   2oc2o 7194   ^m cmap 7490   ~~ cen 7584   Fincfn 7587   Basecbs 15199   +g cplusg 15268   .rcmulr 15269   0gc0g 15416  mrClscmrc 15567   Mndcmnd 16613   MndHom cmhm 16658  SubMndcsubmnd 16659   Grpcgrp 16747   invgcminusg 16748   SymGrpcsymg 17096  pmTrspcpmtr 17160  pmSgncpsgn 17208  pmEvencevpm 17209  mulGrpcmgp 17801   1rcur 17813   Ringcrg 17858   ZRHomczrh 19148   Mat cmat 19509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0