Theorem mdetunilem7 19414

Description: Lemma for mdetuni 19418. (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 5850	. . . . . 6 |- ( c = d -> ( c ` a ) = ( d ` a ) )
2	1	oveq1d 6295	. . . . 5 |- ( c = d -> ( ( c ` a ) F b ) = ( ( d ` a ) F b ) )
3	2	mpt2eq3dv 6346	. . . 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 5855	. . 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 5851	. . . 4 |- ( c = d -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) )
6	5	oveq1d 6295	. . 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 2426	. 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 5850	. . . . . 6 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( c ` a ) = ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) )
9	8	oveq1d 6295	. . . . 5 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( c ` a ) F b ) = ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) )
10	9	mpt2eq3dv 6346	. . . 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 5855	. . 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 5851	. . . 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 6295	. . 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 2426	. 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 5850	. . . . . 6 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( c ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
16	15	oveq1d 6295	. . . . 5 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( c ` a ) F b ) = ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) )
17	16	mpt2eq3dv 6346	. . . 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 5855	. . 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 5851	. . . 4 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) )
20	19	oveq1d 6295	. . 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 2426	. 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 5850	. . . . . 6 |- ( c = E -> ( c ` a ) = ( E ` a ) )
23	22	oveq1d 6295	. . . . 5 |- ( c = E -> ( ( c ` a ) F b ) = ( ( E ` a ) F b ) )
24	23	mpt2eq3dv 6346	. . . 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 5855	. . 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 5851	. . . 4 |- ( c = E -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) )
27	26	oveq1d 6295	. . 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 2426	. 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 2404	. 2 |- ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
30		eqid 2404	. 2 |- ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
31		eqid 2404	. 2 |- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
32		mdetuni.n	. . . 4 |- ( ph -> N e. Fin )
33	32	3ad2ant1 1020	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> N e. Fin )
34		eqid 2404	. . . 4 |- ( SymGrp ` N ) = ( SymGrp ` N )
35	34	symggrp 16751	. . 3 |- ( N e. Fin -> ( SymGrp ` N ) e. Grp )
36		grpmnd 16388	. . 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 2404	. . . 4 |- ran (pmTrsp ` N ) = ran (pmTrsp ` N )
39	38, 34, 31	symgtrf 16820	. . 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 2404	. . . . . 6 |- (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) = (mrCls ` (SubMnd ` ( SymGrp ` N ) ) )
42	38, 34, 31, 41	symggen2 16822	. . . . 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 2412	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) = ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) )
45	44	3ad2ant1 1020	. 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 1020	. . . 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 1020	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> D : B --> K )
50		simp3 1001	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. B )
51	49, 50	ffvelrnd 6012	. . . 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 17544	. . . 4 |- ( ( R e. Ring /\ ( D ` F ) e. K ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
56	47, 51, 55	syl2anc 661	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
57		zrhpsgnmhm 18920	. . . . . . 7 |- ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
58	46, 32, 57	syl2anc 661	. . . . . 6 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
59		eqid 2404	. . . . . . . 8 |- (mulGrp ` R ) = (mulGrp ` R )
60	59, 54	ringidval 17477	. . . . . . 7 |- .1. = ( 0g ` (mulGrp ` R ) )
61	29, 60	mhm0 16300	. . . . . 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 1020	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
64	63	oveq1d 6295	. . 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 16752	. . . . . . . . . . . 12 |- ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
66	32, 65	syl 17	. . . . . . . . . . 11 |- ( ph -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
67	66	3ad2ant1 1020	. . . . . . . . . 10 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
68	67	3ad2ant1 1020	. . . . . . . . 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 5853	. . . . . . . 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 1000	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> a e. N )
71		fvresi 6079	. . . . . . . . 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 2447	. . . . . . 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 6295	. . . . . 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 6344	. . . . 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 19218	. . . . . . . 8 |- ( F e. B -> F e. ( K ^m ( N X. N ) ) )
79	78	3ad2ant3 1022	. . . . . . 7 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. ( K ^m ( N X. N ) ) )
80		elmapi 7480	. . . . . . 7 |- ( F e. ( K ^m ( N X. N ) ) -> F : ( N X. N ) --> K )
81		ffn 5716	. . . . . . 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 6393	. . . . . 6 |- ( F Fn ( N X. N ) <-> F = ( a e. N , b e. N |-> ( a F b ) ) )
84	82, 83	sylib 198	. . . . 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 2448	. . . 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 5855	. . 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 2456	. 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 1000	. . . . . . . . . . . 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 3440	. . . . . . . . . . . . 13 |- ( e e. ran (pmTrsp ` N ) -> e e. ( Base ` ( SymGrp ` N ) ) )
90	89	3ad2ant3 1022	. . . . . . . . . . . 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 16741	. . . . . . . . . . . 12 |- ( ( d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
92	88, 90, 91	syl2anc 661	. . . . . . . . . . 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 5853	. . . . . . . . . 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 1020	. . . . . . . . 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 16734	. . . . . . . . . . . 12 |- ( e e. ( Base ` ( SymGrp ` N ) ) -> e : N -1-1-onto-> N )
96		f1of 5801	. . . . . . . . . . . 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 1020	. . . . . . . . . 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 1000	. . . . . . . . . 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 5928	. . . . . . . . . 10 |- ( ( e : N --> N /\ a e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
101	98, 99, 100	syl2anc 661	. . . . . . . . 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 2445	. . . . . . . 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 6295	. . . . . . 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 6344	. . . . . 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 5855	. . . . 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 16735	. . . . . 6 |- ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N --> N )
107		eqid 2404	. . . . . . . . 9 |- (pmTrsp ` N ) = (pmTrsp ` N )
108	107, 38	pmtrrn2 16811	. . . . . . . 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 1038	. . . . . . . . . . . . . 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 978	. . . . . . . . . . . . . . . 16 |- ( ( c e. N /\ f e. N /\ c =/= f ) <-> ( ( c e. N /\ f e. N ) /\ c =/= f ) )
116	115	biimpri 208	. . . . . . . . . . . . . . 15 |- ( ( ( c e. N /\ f e. N ) /\ c =/= f ) -> ( c e. N /\ f e. N /\ c =/= f ) )
117	116	adantl 466	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
120	119	ad2antrr 726	. . . . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . . . . 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 767	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 6012	. . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . 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 6430	. . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 6012	. . . . . . . . . . . . . . . 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 6430	. . . . . . . . . . . . . . 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 532	. . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 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 1020	. . . . . . . . . . . . . . 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 1063	. . . . . . . . . . . . . . . 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 1000	. . . . . . . . . . . . . . . 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 6012	. . . . . . . . . . . . . . 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 1001	. . . . . . . . . . . . . . 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 6430	. . . . . . . . . . . . . 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 19413	. . . . . . . . . . . . 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 1002	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
141		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = c -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) )
142	32	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
143		simprll 766	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
144		simprlr 767	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
145		simprr 760	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
146	107	pmtrprfv 16804	. . . . . . . . . . . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
148	147	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
149	141, 148	sylan9eqr 2467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = f )
150	149	fveq2d 5855	. . . . . . . . . . . . . . . . . . . 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 6295	. . . . . . . . . . . . . . . . . . 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 3893	. . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . 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 2448	. . . . . . . . . . . . . . . . . 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 5851	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = f -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) )
156		prcom 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { c , f } = { f , c }
157	156	fveq2i 5854	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( (pmTrsp ` N ) ` { c , f } ) = ( (pmTrsp ` N ) ` { f , c } )
158	157	fveq1i 5852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( (pmTrsp ` N ) ` { f , c } ) ` f )
159	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
160		simplrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
161	160	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
162	160	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
163		simplrr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
164	163	necomd 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
165	107	pmtrprfv 16804	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
167	158, 166	syl5eq 2457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = c )
168	155, 167	sylan9eqr 2467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = c )
169	168	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . . . 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 6295	. . . . . . . . . . . . . . . . . . . . . 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 3893	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
172	171	adantl 466	. . . . . . . . . . . . . . . . . . . . . 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 2448	. . . . . . . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . . . . . . 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 3064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- a e. _V
176	175	elpr 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. { c , f } <-> ( a = c \/ a = f ) )
177	176	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
178		ioran 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
179	177, 178	bitr2i 252	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -. a = c /\ -. a = f ) <-> -. a e. { c , f } )
180	179	biimpi 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
181	180	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
182		prssi 4130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( c e. N /\ f e. N ) -> { c , f } C_ N )
183	160, 182	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } C_ N )
184		pr2ne 8417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( c e. N /\ f e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
185	160, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( { c , f } ~~ 2o <-> c =/= f ) )
186	163, 185	mpbird 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
187	107	pmtrmvd 16807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
188	159, 183, 186, 187	syl3anc 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
189	188	eleq2d 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
190	189	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 } ) )
191	190	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
192	181, 191	mpbird 234	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
193	107	pmtrf 16806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
194	159, 183, 186, 193	syl3anc 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
195		ffn 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( (pmTrsp ` N ) ` { c , f } ) : N --> N -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
196	194, 195	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) Fn N )
197		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
198		fnelnfp 6083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) =/= a ) )
199	198	necon2bbid 2661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( (pmTrsp ` N ) ` { c , f } ) Fn N /\ a e. N ) -> ( ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a <-> -. a e. dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) ) )
200	196, 197, 199	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
201	200	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
202	192, 201	mpbird 234	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = a )
203	202	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . . 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 ) )
204	203	oveq1d 6295	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = ( ( d ` a ) F b ) )
205		iffalse 3896	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
206	205	adantl 466	. . . . . . . . . . . . . . . . . . . . 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 ) )
207	204, 206	eqtr4d 2448	. . . . . . . . . . . . . . . . . . . 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 ) ) )
208	174, 207	pm2.61dan 794	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) -> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) = if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) )
209		iffalse 3896	. . . . . . . . . . . . . . . . . . . 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 ) ) )
210	209	adantl 466	. . . . . . . . . . . . . . . . . . 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 ) ) )
211	208, 210	eqtr4d 2448	. . . . . . . . . . . . . . . . . 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 ) ) ) )
212	154, 211	pm2.61dan 794	. . . . . . . . . . . . . . . . 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 ) ) ) )
213	212	3adant3 1019	. . . . . . . . . . . . . . . 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 ) ) ) )
214	213	mpt2eq3dva 6344	. . . . . . . . . . . . . . 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 ) ) ) ) )
215	140, 214	sylan 471	. . . . . . . . . . . . . 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 ) ) ) ) )
216	215	fveq2d 5855	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = c , ( ( d ` f ) F b ) , if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) ) ) ) )
217		fveq2 5851	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = c -> ( d ` a ) = ( d ` c ) )
218	217	oveq1d 6295	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
219		iftrue 3893	. . . . . . . . . . . . . . . . . . . 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 ) )
220	218, 219	eqtr4d 2448	. . . . . . . . . . . . . . . . . . 19 |- ( a = c -> ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) ) )
221		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = f -> ( d ` a ) = ( d ` f ) )
222	221	oveq1d 6295	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
223		iftrue 3893	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
224	222, 223	eqtr4d 2448	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
225	224	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
226		iffalse 3896	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
227	226	eqcomd 2412	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
228	227	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ -. a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
229	225, 228	pm2.61dan 794	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
230		iffalse 3896	. . . . . . . . . . . . . . . . . . . 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 ) ) )
231	229, 230	eqtr4d 2448	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
232	220, 231	pm2.61i 166	. . . . . . . . . . . . . . . . . 18 |- ( ( d ` a ) F b ) = if ( a = c , ( ( d ` c ) F b ) , if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
233	232	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 ) ) ) )
234	233	mpt2eq3ia 6345	. . . . . . . . . . . . . . . 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 ) ) ) )
235	234	fveq2i 5854	. . . . . . . . . . . . . . 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 ) ) ) ) )
236	235	fveq2i 5854	. . . . . . . . . . . . . 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 ) ) ) ) ) )
237	236	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 ) ) ) ) ) ) )
238	139, 216, 237	3eqtr4d 2455	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( D ` ( a e. N , b e. N |-> ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
239		fveq1 5850	. . . . . . . . . . . . . . . . 17 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) )
240	239	fveq2d 5855	. . . . . . . . . . . . . . . 16 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) )
241	240	oveq1d 6295	. . . . . . . . . . . . . . 15 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
242	241	mpt2eq3dv 6346	. . . . . . . . . . . . . 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 ) ) )
243	242	fveq2d 5855	. . . . . . . . . . . . 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 ) ) ) )
244	243	eqeq1d 2406	. . . . . . . . . . . 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 ) ) ) ) ) )
245	238, 244	syl5ibrcom 224	. . . . . . . . . . 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 ) ) ) ) ) )
246	245	expr 615	. . . . . . . . . 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 ) ) ) ) ) ) )
247	246	impd 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 ) ) ) ) ) )
248	247	rexlimdvva 2905	. . . . . . . 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 ) ) ) ) ) )
249	108, 248	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 ) ) ) ) ) )
250	249	3impia 1196	. . . . . 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 ) ) ) ) )
251	106, 250	syl3an2 1266	. . . . 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 ) ) ) ) )
252	105, 251	eqtrd 2445	. . . 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 ) ) ) ) )
253	252	adantr 465	. . 3 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) )
254		fveq2 5851	. . . 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 ) ) ) )
255	254	adantl 466	. . 3 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) ) = ( ( invg ` R ) ` ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) )
256		eqid 2404	. . . . . 6 |- ( invg ` R ) = ( invg ` R )
257	47	3ad2ant1 1020	. . . . . 6 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> R e. Ring )
258	58	3ad2ant1 1020	. . . . . . . . 9 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
259	258	3ad2ant1 1020	. . . . . . . 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 ) ) )
260	59, 52	mgpbas 17469	. . . . . . . . 9 |- K = ( Base ` (mulGrp ` R ) )
261	31, 260	mhmf 16297	. . . . . . . 8 |- ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
262	259, 261	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 )
263	262, 88	ffvelrnd 6012	. . . . . 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 )
264	49	3ad2ant1 1020	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> D : B --> K )
265		simp13 1031	. . . . . . 7 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> F e. B )
266	264, 265	ffvelrnd 6012	. . . . . 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 )
267	52, 53, 256, 257, 263, 266	ringmneg1 17564	. . . . 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 ) ) ) )
268	59, 53	mgpplusg 17467	. . . . . . . . 9 |- .x. = ( +g ` (mulGrp ` R ) )
269	31, 30, 268	mhmlin 16299	. . . . . . . 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 ) ) )
270	259, 88, 90, 269	syl3anc 1232	. . . . . . 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 ) ) )
271	33	3ad2ant1 1020	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> N e. Fin )
272		simp3 1001	. . . . . . . . . 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 ) )
273	34, 31, 38	pmtrodpm 18933	. . . . . . . . . 10 |- ( ( N e. Fin /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
274	271, 272, 273	syl2anc 661	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
275		eqid 2404	. . . . . . . . . 10 |- ( ZRHom ` R ) = ( ZRHom ` R )
276		eqid 2404	. . . . . . . . . 10 |- (pmSgn ` N ) = (pmSgn ` N )
277	275, 276, 54, 31, 256	zrhpsgnodpm 18928	. . . . . . . . 9 |- ( ( R e. Ring /\ N e. Fin /\ e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` e ) = ( ( invg ` R ) ` .1. ) )
278	257, 271, 274, 277	syl3anc 1232	. . . . . . . 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. ) )
279	278	oveq2d 6296	. . . . . . 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. ) ) )
280	52, 53, 54, 256, 257, 263	rngnegr 17563	. . . . . . 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 ) ) )
281	270, 279, 280	3eqtrrd 2450	. . . . . 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 ) ) )
282	281	oveq1d 6295	. . . . 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 ) ) )
283	267, 282	eqtr3d 2447	. . . 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 ) ) )
284	283	adantr 465	. . 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 ) ) )
285	253, 255, 284	3eqtrd 2449	. 2 |- ( ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ran (pmTrsp ` N ) ) /\ ( D ` ( a e. N , b e. N |-> ( ( d ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) .x. ( D ` F ) ) ) -> ( D ` ( a e. N , b e. N |-> ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( d ( +g ` ( SymGrp ` N ) ) e ) ) .x. ( D ` F ) ) )
286		simp2 1000	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
287	34, 31	elsymgbas 16733	. . . 4 |- ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
288	33, 287	syl 17	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
289	286, 288	mpbird 234	. 2 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E e. ( Base ` ( SymGrp ` N ) ) )
290	7, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 285, 289	mrcmndind 16323	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 186   \/ wo 368   /\ wa 369   /\ w3a 976   = wceq 1407   e. wcel 1844   =/= wne 2600   A.wral 2756   E.wrex 2757   \ cdif 3413   C_ wss 3416   ifcif 3887   {csn 3974   {cpr 3976   class class class wbr 4397   _I cid 4735   X. cxp 4823   dom cdm 4825   ran crn 4826   |` cres 4827   o. ccom 4829   Fn wfn 5566   -->wf 5567   -1-1-onto->wf1o 5570   ` cfv 5571  (class class class)co 6280   |-> cmpt2 6282   oFcof 6521   2oc2o 7163   ^m cmap 7459   ~~ cen 7553   Fincfn 7556   Basecbs 14843   +g cplusg 14911   .rcmulr 14912   0gc0g 15056  mrClscmrc 15199   Mndcmnd 16245   MndHom cmhm 16290  SubMndcsubmnd 16291   Grpcgrp 16379   invgcminusg 16380   SymGrpcsymg 16728  pmTrspcpmtr 16792  pmSgncpsgn 16840  pmEvencevpm 16841  mulGrpcmgp 17463   1rcur 17475   Ringcrg 17520   ZRHomczrh 18839   Mat cmat 19203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584