Theorem mdetunilem7 18324

Description: Lemma for mdetuni 18328. (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 5687	. . . . . 6 |- ( c = d -> ( c ` a ) = ( d ` a ) )
2	1	oveq1d 6105	. . . . 5 |- ( c = d -> ( ( c ` a ) F b ) = ( ( d ` a ) F b ) )
3	2	mpt2eq3dv 6151	. . . 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 5692	. . 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 5688	. . . 4 |- ( c = d -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) )
6	5	oveq1d 6105	. . 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 2455	. 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 5687	. . . . . 6 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( c ` a ) = ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) )
9	8	oveq1d 6105	. . . . 5 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( c ` a ) F b ) = ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) )
10	9	mpt2eq3dv 6151	. . . 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 5692	. . 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 5688	. . . 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 6105	. . 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 2455	. 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 5687	. . . . . 6 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( c ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
16	15	oveq1d 6105	. . . . 5 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( c ` a ) F b ) = ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) )
17	16	mpt2eq3dv 6151	. . . 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 5692	. . 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 5688	. . . 4 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) )
20	19	oveq1d 6105	. . 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 2455	. 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 5687	. . . . . 6 |- ( c = E -> ( c ` a ) = ( E ` a ) )
23	22	oveq1d 6105	. . . . 5 |- ( c = E -> ( ( c ` a ) F b ) = ( ( E ` a ) F b ) )
24	23	mpt2eq3dv 6151	. . . 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 5692	. . 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 5688	. . . 4 |- ( c = E -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) )
27	26	oveq1d 6105	. . 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 2455	. 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 2441	. 2 |- ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
30		eqid 2441	. 2 |- ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
31		eqid 2441	. 2 |- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
32		mdetuni.n	. . . 4 |- ( ph -> N e. Fin )
33	32	3ad2ant1 1004	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> N e. Fin )
34		eqid 2441	. . . 4 |- ( SymGrp ` N ) = ( SymGrp ` N )
35	34	symggrp 15898	. . 3 |- ( N e. Fin -> ( SymGrp ` N ) e. Grp )
36		grpmnd 15543	. . 3 |- ( ( SymGrp ` N ) e. Grp -> ( SymGrp ` N ) e. Mnd )
37	33, 35, 36	3syl 20	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( SymGrp ` N ) e. Mnd )
38		eqid 2441	. . . 4 |- ran (pmTrsp ` N ) = ran (pmTrsp ` N )
39	38, 34, 31	symgtrf 15968	. . 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 2441	. . . . . 6 |- (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) = (mrCls ` (SubMnd ` ( SymGrp ` N ) ) )
42	38, 34, 31, 41	symggen2 15970	. . . . 5 |- ( N e. Fin -> ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
43	32, 42	syl 16	. . . 4 |- ( ph -> ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) = ( Base ` ( SymGrp ` N ) ) )
44	43	eqcomd 2446	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) = ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) )
45	44	3ad2ant1 1004	. 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 1004	. . . 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 1004	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> D : B --> K )
50		simp3 985	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. B )
51	49, 50	ffvelrnd 5841	. . . 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	rnglidm 16658	. . . 4 |- ( ( R e. Ring /\ ( D ` F ) e. K ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
56	47, 51, 55	syl2anc 656	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
57		zrhpsgnmhm 17914	. . . . . . 7 |- ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
58	46, 32, 57	syl2anc 656	. . . . . 6 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
59		eqid 2441	. . . . . . . 8 |- (mulGrp ` R ) = (mulGrp ` R )
60	59, 54	rngidval 16595	. . . . . . 7 |- .1. = ( 0g ` (mulGrp ` R ) )
61	29, 60	mhm0 15468	. . . . . 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 16	. . . . 5 |- ( ph -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
63	62	3ad2ant1 1004	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
64	63	oveq1d 6105	. . 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 15899	. . . . . . . . . . . 12 |- ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
66	32, 65	syl 16	. . . . . . . . . . 11 |- ( ph -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
67	66	3ad2ant1 1004	. . . . . . . . . 10 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
68	67	3ad2ant1 1004	. . . . . . . . 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 5690	. . . . . . . 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 984	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> a e. N )
71		fvresi 5901	. . . . . . . . 9 |- ( a e. N -> ( ( _I |` N ) ` a ) = a )
72	70, 71	syl 16	. . . . . . . 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 2475	. . . . . . 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 6105	. . . . . 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 6149	. . . . 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 18223	. . . . . . . 8 |- ( F e. B -> F e. ( K ^m ( N X. N ) ) )
79	78	3ad2ant3 1006	. . . . . . 7 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. ( K ^m ( N X. N ) ) )
80		elmapi 7230	. . . . . . 7 |- ( F e. ( K ^m ( N X. N ) ) -> F : ( N X. N ) --> K )
81		ffn 5556	. . . . . . 7 |- ( F : ( N X. N ) --> K -> F Fn ( N X. N ) )
82	79, 80, 81	3syl 20	. . . . . 6 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F Fn ( N X. N ) )
83		fnov 6197	. . . . . 6 |- ( F Fn ( N X. N ) <-> F = ( a e. N , b e. N |-> ( a F b ) ) )
84	82, 83	sylib 196	. . . . 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 2476	. . . 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 5692	. . 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 2484	. 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 984	. . . . . . . . . . . 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 3349	. . . . . . . . . . . . 13 |- ( e e. ran (pmTrsp ` N ) -> e e. ( Base ` ( SymGrp ` N ) ) )
90	89	3ad2ant3 1006	. . . . . . . . . . . 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 15888	. . . . . . . . . . . 12 |- ( ( d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
92	88, 90, 91	syl2anc 656	. . . . . . . . . . 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 5690	. . . . . . . . . 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 1004	. . . . . . . . 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 15881	. . . . . . . . . . . 12 |- ( e e. ( Base ` ( SymGrp ` N ) ) -> e : N -1-1-onto-> N )
96		f1of 5638	. . . . . . . . . . . 12 |- ( e : N -1-1-onto-> N -> e : N --> N )
97	90, 95, 96	3syl 20	. . . . . . . . . . 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 1004	. . . . . . . . . 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 984	. . . . . . . . . 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 5765	. . . . . . . . . 10 |- ( ( e : N --> N /\ a e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
101	98, 99, 100	syl2anc 656	. . . . . . . . 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 2473	. . . . . . . 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 6105	. . . . . . 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 6149	. . . . . 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 5692	. . . . 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	symgbasf1o 15881	. . . . . . 7 |- ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N -1-1-onto-> N )
107		f1of 5638	. . . . . . 7 |- ( d : N -1-1-onto-> N -> d : N --> N )
108	106, 107	syl 16	. . . . . 6 |- ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N --> N )
109		eqid 2441	. . . . . . . . 9 |- (pmTrsp ` N ) = (pmTrsp ` N )
110	109, 38	pmtrrn2 15959	. . . . . . . 8 |- ( e e. ran (pmTrsp ` N ) -> E. c e. N E. f e. N ( c =/= f /\ e = ( (pmTrsp ` N ) ` { c , f } ) ) )
111		mdetuni.0g	. . . . . . . . . . . . . 14 |- .0. = ( 0g ` R )
112		mdetuni.pg	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
113		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. ) )
114		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 ) ) ) )
115		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 ) ) ) )
116		simpll1 1022	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ph )
117		df-3an 962	. . . . . . . . . . . . . . . 16 |- ( ( c e. N /\ f e. N /\ c =/= f ) <-> ( ( c e. N /\ f e. N ) /\ c =/= f ) )
118	117	biimpri 206	. . . . . . . . . . . . . . 15 |- ( ( ( c e. N /\ f e. N ) /\ c =/= f ) -> ( c e. N /\ f e. N /\ c =/= f ) )
119	118	adantl 463	. . . . . . . . . . . . . 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 ) )
120	79, 80	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F : ( N X. N ) --> K )
121	120	adantr 462	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
122	121	ad2antrr 720	. . . . . . . . . . . . . . . 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 )
123		simpllr 753	. . . . . . . . . . . . . . . . 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 )
124		simprlr 757	. . . . . . . . . . . . . . . . . 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 )
125	124	adantr 462	. . . . . . . . . . . . . . . . 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 )
126	123, 125	ffvelrnd 5841	. . . . . . . . . . . . . . . 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 )
127		simpr 458	. . . . . . . . . . . . . . . 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 )
128	122, 126, 127	fovrnd 6234	. . . . . . . . . . . . . . 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 )
129		simprll 756	. . . . . . . . . . . . . . . . . 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 )
130	129	adantr 462	. . . . . . . . . . . . . . . . 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 )
131	123, 130	ffvelrnd 5841	. . . . . . . . . . . . . . . 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 )
132	122, 131, 127	fovrnd 6234	. . . . . . . . . . . . . . 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 )
133	128, 132	jca 529	. . . . . . . . . . . . . 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 ) )
134	120	ad2antrr 720	. . . . . . . . . . . . . . . 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 )
135	134	3ad2ant1 1004	. . . . . . . . . . . . . . 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 )
136		simp1lr 1047	. . . . . . . . . . . . . . . 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 )
137		simp2 984	. . . . . . . . . . . . . . . 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 )
138	136, 137	ffvelrnd 5841	. . . . . . . . . . . . . . 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 )
139		simp3 985	. . . . . . . . . . . . . . 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 )
140	135, 138, 139	fovrnd 6234	. . . . . . . . . . . . . 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 )
141	76, 77, 52, 111, 54, 112, 53, 32, 46, 48, 113, 114, 115, 116, 119, 133, 140	mdetunilem6 18323	. . . . . . . . . . . . 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 ) ) ) ) ) ) )
142		simpl1 986	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
143		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = c -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) )
144	32	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
145		simprll 756	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
146		simprlr 757	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
147		simprr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
148	109	pmtrprfv 15952	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( N e. Fin /\ ( c e. N /\ f e. N /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
149	144, 145, 146, 147, 148	syl13anc 1215	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
150	149	adantr 462	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
151	143, 150	sylan9eqr 2495	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = f )
152	151	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` f ) )
153	152	oveq1d 6105	. . . . . . . . . . . . . . . . . . 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 ) )
154		iftrue 3794	. . . . . . . . . . . . . . . . . . . 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 ) )
155	154	adantl 463	. . . . . . . . . . . . . . . . . . 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 ) )
156	153, 155	eqtr4d 2476	. . . . . . . . . . . . . . . . . 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 ) ) ) )
157		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = f -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) )
158		prcom 3950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { c , f } = { f , c }
159	158	fveq2i 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( (pmTrsp ` N ) ` { c , f } ) = ( (pmTrsp ` N ) ` { f , c } )
160	159	fveq1i 5689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( (pmTrsp ` N ) ` { f , c } ) ` f )
161	32	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
162		simplrl 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
163	162	simprd 460	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
164	162	simpld 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
165		simplrr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
166	165	necomd 2693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
167	109	pmtrprfv 15952	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. Fin /\ ( f e. N /\ c e. N /\ f =/= c ) ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
168	161, 163, 164, 166, 167	syl13anc 1215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
169	160, 168	syl5eq 2485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = c )
170	157, 169	sylan9eqr 2495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = c )
171	170	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) = ( d ` c ) )
172	171	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . 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 ) )
173		iftrue 3794	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
174	173	adantl 463	. . . . . . . . . . . . . . . . . . . . . 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 ) )
175	172, 174	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
176	175	adantlr 709	. . . . . . . . . . . . . . . . . . . 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 ) ) )
177		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- a e. _V
178	177	elpr 3892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. { c , f } <-> ( a = c \/ a = f ) )
179	178	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
180		ioran 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
181	179, 180	bitr2i 250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -. a = c /\ -. a = f ) <-> -. a e. { c , f } )
182	181	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
183	182	adantll 708	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
184		prssi 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( c e. N /\ f e. N ) -> { c , f } C_ N )
185	162, 184	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } C_ N )
186		pr2ne 8168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( c e. N /\ f e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
187	162, 186	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
188	165, 187	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
189	109	pmtrmvd 15955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
190	161, 185, 188, 189	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
191	190	eleq2d 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
192	191	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
193	192	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
194	183, 193	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
195	109	pmtrf 15954	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
196	161, 185, 188, 195	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
197		ffn 5556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( (pmTrsp ` N ) ` { c , f } ) : N --> N -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
198	196, 197	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
199		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
200		fnelnfp 5905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) =/= a ) )
201	200	necon2bbid 2667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
202	198, 199, 201	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
203	202	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
204	194, 203	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a )
205	204	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . 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 ) )
206	205	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . 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 ) )
207		iffalse 3796	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
208	207	adantl 463	. . . . . . . . . . . . . . . . . . . . 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 ) )
209	206, 208	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . 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 ) ) )
210	176, 209	pm2.61dan 784	. . . . . . . . . . . . . . . . . . 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 ) ) )
211		iffalse 3796	. . . . . . . . . . . . . . . . . . . 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 ) ) )
212	211	adantl 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
213	210, 212	eqtr4d 2476	. . . . . . . . . . . . . . . . . 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 ) ) ) )
214	156, 213	pm2.61dan 784	. . . . . . . . . . . . . . . . 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 ) ) ) )
215	214	3adant3 1003	. . . . . . . . . . . . . . . 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 ) ) ) )
216	215	mpt2eq3dva 6149	. . . . . . . . . . . . . . 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 ) ) ) ) )
217	142, 216	sylan 468	. . . . . . . . . . . . . 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 ) ) ) ) )
218	217	fveq2d 5692	. . . . . . . . . . . . 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 ) ) ) ) ) )
219		fveq2 5688	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = c -> ( d ` a ) = ( d ` c ) )
220	219	oveq1d 6105	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
221		iftrue 3794	. . . . . . . . . . . . . . . . . . . 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 ) )
222	220, 221	eqtr4d 2476	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
223		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = f -> ( d ` a ) = ( d ` f ) )
224	223	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
225		iftrue 3794	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
226	224, 225	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
227	226	adantl 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
228		iffalse 3796	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
229	228	eqcomd 2446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
230	229	adantl 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ -. a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
231	227, 230	pm2.61dan 784	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
232		iffalse 3796	. . . . . . . . . . . . . . . . . . . 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 ) ) )
233	231, 232	eqtr4d 2476	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
234	222, 233	pm2.61i 164	. . . . . . . . . . . . . . . . . 18 |- ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
235	234	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 ) ) ) )
236	235	mpt2eq3ia 6150	. . . . . . . . . . . . . . . 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 ) ) ) )
237	236	fveq2i 5691	. . . . . . . . . . . . . . 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 ) ) ) ) )
238	237	fveq2i 5691	. . . . . . . . . . . . . 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 ) ) ) ) ) )
239	238	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 ) ) ) ) ) ) )
240	141, 218, 239	3eqtr4d 2483	. . . . . . . . . . . 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 ) ) ) ) )
241		fveq1 5687	. . . . . . . . . . . . . . . . 17 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) )
242	241	fveq2d 5692	. . . . . . . . . . . . . . . 16 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) )
243	242	oveq1d 6105	. . . . . . . . . . . . . . 15 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
244	243	mpt2eq3dv 6151	. . . . . . . . . . . . . 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 ) ) )
245	244	fveq2d 5692	. . . . . . . . . . . . 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 ) ) ) )
246	245	eqeq1d 2449	. . . . . . . . . . . 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 ) ) ) ) ) )
247	240, 246	syl5ibrcom 222	. . . . . . . . . . 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 ) ) ) ) ) )
248	247	expr 612	. . . . . . . . . 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 ) ) ) ) ) ) )
249	248	imp3a 431	. . . . . . . . 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 ) ) ) ) ) )
250	249	rexlimdvva 2846	. . . . . . . 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 ) ) ) ) ) )
251	110, 250	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 ) ) ) ) ) )
252	251	3impia 1179	. . . . . 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 ) ) ) ) )
253	108, 252	syl3an2 1247	. . . . 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 ) ) ) ) )
254	105, 253	eqtrd 2473	. . . 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 ) ) ) ) )
255	254	adantr 462	. . 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 ) ) ) ) )
256		fveq2 5688	. . . 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 ) ) ) )
257	256	adantl 463	. . 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 ) ) ) )
258		eqid 2441	. . . . . 6 |- ( invg ` R ) = ( invg ` R )
259	47	3ad2ant1 1004	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> R e. Ring )
260	58	3ad2ant1 1004	. . . . . . . . 9 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
261	260	3ad2ant1 1004	. . . . . . . 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 ) ) )
262	59, 52	mgpbas 16587	. . . . . . . . 9 |- K = ( Base ` (mulGrp ` R ) )
263	31, 262	mhmf 15465	. . . . . . . 8 |- ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
264	261, 263	syl 16	. . . . . . 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 )
265	264, 88	ffvelrnd 5841	. . . . . 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 )
266	49	3ad2ant1 1004	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> D : B --> K )
267		simp13 1015	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> F e. B )
268	266, 267	ffvelrnd 5841	. . . . . 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 )
269	52, 53, 258, 259, 265, 268	rngmneg1 16677	. . . . 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 ) ) ) )
270	59, 53	mgpplusg 16585	. . . . . . . . 9 |- .x. = ( +g ` (mulGrp ` R ) )
271	31, 30, 270	mhmlin 15467	. . . . . . . 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 ) ) )
272	261, 88, 90, 271	syl3anc 1213	. . . . . . 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 ) ) )
273	33	3ad2ant1 1004	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> N e. Fin )
274		simp3 985	. . . . . . . . . 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 ) )
275	34, 31, 38	pmtrodpm 17927	. . . . . . . . . 10 |- ( ( N e. Fin /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
276	273, 274, 275	syl2anc 656	. . . . . . . . 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 ) ) )
277		eqid 2441	. . . . . . . . . 10 |- ( ZRHom ` R ) = ( ZRHom ` R )
278		eqid 2441	. . . . . . . . . 10 |- (pmSgn ` N ) = (pmSgn ` N )
279	277, 278, 54, 31, 258	zrhpsgnodpm 17922	. . . . . . . . 9 |- ( ( R e. Ring /\ N e. Fin /\ e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
280	259, 273, 276, 279	syl3anc 1213	. . . . . . . 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. ) )
281	280	oveq2d 6106	. . . . . . 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. ) ) )
282	52, 53, 54, 258, 259, 265	rngnegr 16676	. . . . . . 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 ) ) )
283	272, 281, 282	3eqtrrd 2478	. . . . . 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 ) ) )
284	283	oveq1d 6105	. . . . 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 ) ) )
285	269, 284	eqtr3d 2475	. . . 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 ) ) )
286	285	adantr 462	. . 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 ) ) )
287	255, 257, 286	3eqtrd 2477	. 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 ) ) )
288		simp2 984	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
289	34, 31	elsymgbas 15880	. . . 4 |- ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
290	33, 289	syl 16	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
291	288, 290	mpbird 232	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E e. ( Base ` ( SymGrp ` N ) ) )
292	7, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 287, 291	mrcmndind 15489	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 184   \/ wo 368   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   \ cdif 3322   C_ wss 3325   ifcif 3788   {csn 3874   {cpr 3876   class class class wbr 4289   _I cid 4627   X. cxp 4834   dom cdm 4836   ran crn 4837   |` cres 4838   o. ccom 4840   Fn wfn 5410   -->wf 5411   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   e. cmpt2 6092   oFcof 6317   2oc2o 6910   ^m cmap 7210   ~~ cen 7303   Fincfn 7306   Basecbs 14170   +g cplusg 14234   .rcmulr 14235   0gc0g 14374  mrClscmrc 14517   Mndcmnd 15405   Grpcgrp 15406   invgcminusg 15407   MndHom cmhm 15458  SubMndcsubmnd 15459   SymGrpcsymg 15875  pmTrspcpmtr 15940  pmSgncpsgn 15988  pmEvencevpm 15989  mulGrpcmgp 16581   1rcur 16593   Ringcrg 16635   ZRHomczrh 17831   Mat cmat 18180

This theorem was proved from axi