Theorem mdetunilem7 19643

Description: Lemma for mdetuni 19647. (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 5864	. . . . . 6 |- ( c = d -> ( c ` a ) = ( d ` a ) )
2	1	oveq1d 6305	. . . . 5 |- ( c = d -> ( ( c ` a ) F b ) = ( ( d ` a ) F b ) )
3	2	mpt2eq3dv 6357	. . . 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 5869	. . 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 5865	. . . 4 |- ( c = d -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` d ) )
6	5	oveq1d 6305	. . 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 2466	. 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 5864	. . . . . 6 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( c ` a ) = ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) )
9	8	oveq1d 6305	. . . . 5 |- ( c = ( d ( +g ` ( SymGrp ` N ) ) e ) -> ( ( c ` a ) F b ) = ( ( ( d ( +g ` ( SymGrp ` N ) ) e ) ` a ) F b ) )
10	9	mpt2eq3dv 6357	. . . 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 5869	. . 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 5865	. . . 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 6305	. . 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 2466	. 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 5864	. . . . . 6 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( c ` a ) = ( ( 0g ` ( SymGrp ` N ) ) ` a ) )
16	15	oveq1d 6305	. . . . 5 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( c ` a ) F b ) = ( ( ( 0g ` ( SymGrp ` N ) ) ` a ) F b ) )
17	16	mpt2eq3dv 6357	. . . 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 5869	. . 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 5865	. . . 4 |- ( c = ( 0g ` ( SymGrp ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) )
20	19	oveq1d 6305	. . 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 2466	. 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 5864	. . . . . 6 |- ( c = E -> ( c ` a ) = ( E ` a ) )
23	22	oveq1d 6305	. . . . 5 |- ( c = E -> ( ( c ` a ) F b ) = ( ( E ` a ) F b ) )
24	23	mpt2eq3dv 6357	. . . 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 5869	. . 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 5865	. . . 4 |- ( c = E -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` c ) = ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) )
27	26	oveq1d 6305	. . 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 2466	. 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 2451	. 2 |- ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
30		eqid 2451	. 2 |- ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
31		eqid 2451	. 2 |- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
32		mdetuni.n	. . . 4 |- ( ph -> N e. Fin )
33	32	3ad2ant1 1029	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> N e. Fin )
34		eqid 2451	. . . 4 |- ( SymGrp ` N ) = ( SymGrp ` N )
35	34	symggrp 17041	. . 3 |- ( N e. Fin -> ( SymGrp ` N ) e. Grp )
36		grpmnd 16678	. . 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 2451	. . . 4 |- ran (pmTrsp ` N ) = ran (pmTrsp ` N )
39	38, 34, 31	symgtrf 17110	. . 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 2451	. . . . . 6 |- (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) = (mrCls ` (SubMnd ` ( SymGrp ` N ) ) )
42	38, 34, 31, 41	symggen2 17112	. . . . 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 2457	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) = ( (mrCls ` (SubMnd ` ( SymGrp ` N ) ) ) ` ran (pmTrsp ` N ) ) )
45	44	3ad2ant1 1029	. 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 1029	. . . 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 1029	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> D : B --> K )
50		simp3 1010	. . . . 5 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. B )
51	49, 50	ffvelrnd 6023	. . . 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 17804	. . . 4 |- ( ( R e. Ring /\ ( D ` F ) e. K ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
56	47, 51, 55	syl2anc 667	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( .1. .x. ( D ` F ) ) = ( D ` F ) )
57		zrhpsgnmhm 19152	. . . . . . 7 |- ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
58	46, 32, 57	syl2anc 667	. . . . . 6 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
59		eqid 2451	. . . . . . . 8 |- (mulGrp ` R ) = (mulGrp ` R )
60	59, 54	ringidval 17737	. . . . . . 7 |- .1. = ( 0g ` (mulGrp ` R ) )
61	29, 60	mhm0 16590	. . . . . 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 1029	. . . 4 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = .1. )
64	63	oveq1d 6305	. . 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 17042	. . . . . . . . . . . 12 |- ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
66	32, 65	syl 17	. . . . . . . . . . 11 |- ( ph -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
67	66	3ad2ant1 1029	. . . . . . . . . 10 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
68	67	3ad2ant1 1029	. . . . . . . . 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 5867	. . . . . . . 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 1009	. . . . . . . . 9 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ a e. N /\ b e. N ) -> a e. N )
71		fvresi 6090	. . . . . . . . 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 2487	. . . . . . 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 6305	. . . . . 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 6355	. . . . 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 19447	. . . . . . . 8 |- ( F e. B -> F e. ( K ^m ( N X. N ) ) )
79	78	3ad2ant3 1031	. . . . . . 7 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> F e. ( K ^m ( N X. N ) ) )
80		elmapi 7493	. . . . . . 7 |- ( F e. ( K ^m ( N X. N ) ) -> F : ( N X. N ) --> K )
81		ffn 5728	. . . . . . 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 6404	. . . . . 6 |- ( F Fn ( N X. N ) <-> F = ( a e. N , b e. N |-> ( a F b ) ) )
84	82, 83	sylib 200	. . . . 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 2488	. . . 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 5869	. . 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 2496	. 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 1009	. . . . . . . . . . . 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 3428	. . . . . . . . . . . . 13 |- ( e e. ran (pmTrsp ` N ) -> e e. ( Base ` ( SymGrp ` N ) ) )
90	89	3ad2ant3 1031	. . . . . . . . . . . 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 17031	. . . . . . . . . . . 12 |- ( ( d e. ( Base ` ( SymGrp ` N ) ) /\ e e. ( Base ` ( SymGrp ` N ) ) ) -> ( d ( +g ` ( SymGrp ` N ) ) e ) = ( d o. e ) )
92	88, 90, 91	syl2anc 667	. . . . . . . . . . 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 5867	. . . . . . . . . 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 1029	. . . . . . . . 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 17024	. . . . . . . . . . . 12 |- ( e e. ( Base ` ( SymGrp ` N ) ) -> e : N -1-1-onto-> N )
96		f1of 5814	. . . . . . . . . . . 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 1029	. . . . . . . . . 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 1009	. . . . . . . . . 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 5942	. . . . . . . . . 10 |- ( ( e : N --> N /\ a e. N ) -> ( ( d o. e ) ` a ) = ( d ` ( e ` a ) ) )
101	98, 99, 100	syl2anc 667	. . . . . . . . 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 2485	. . . . . . . 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 6305	. . . . . . 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 6355	. . . . . 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 5869	. . . . 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 17025	. . . . . 6 |- ( d e. ( Base ` ( SymGrp ` N ) ) -> d : N --> N )
107		eqid 2451	. . . . . . . . 9 |- (pmTrsp ` N ) = (pmTrsp ` N )
108	107, 38	pmtrrn2 17101	. . . . . . . 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 1047	. . . . . . . . . . . . . 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 987	. . . . . . . . . . . . . . . 16 |- ( ( c e. N /\ f e. N /\ c =/= f ) <-> ( ( c e. N /\ f e. N ) /\ c =/= f ) )
116	115	biimpri 210	. . . . . . . . . . . . . . 15 |- ( ( ( c e. N /\ f e. N ) /\ c =/= f ) -> ( c e. N /\ f e. N /\ c =/= f ) )
117	116	adantl 468	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> F : ( N X. N ) --> K )
120	119	ad2antrr 732	. . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 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 6023	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 6441	. . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 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 6023	. . . . . . . . . . . . . . . 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 6441	. . . . . . . . . . . . . . 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 535	. . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . 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 1029	. . . . . . . . . . . . . . 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 1072	. . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . 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 6023	. . . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . . . 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 6441	. . . . . . . . . . . . . 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 19642	. . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) /\ d : N --> N ) -> ph )
141		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = c -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) )
142	32	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> N e. Fin )
143		simprll 772	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c e. N )
144		simprlr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> f e. N )
145		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> c =/= f )
146	107	pmtrprfv 17094	. . . . . . . . . . . . . . . . . . . . . . . 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 1270	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
148	147	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` c ) = f )
149	141, 148	sylan9eqr 2507	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = c ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = f )
150	149	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . . . . . 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 3887	. . . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = f -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) )
156		prcom 4050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { c , f } = { f , c }
157	156	fveq2i 5868	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( (pmTrsp ` N ) ` { c , f } ) = ( (pmTrsp ` N ) ` { f , c } )
158	157	fveq1i 5866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = ( ( (pmTrsp ` N ) ` { f , c } ) ` f )
159	32	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> N e. Fin )
160		simplrl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( c e. N /\ f e. N ) )
161	160	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f e. N )
162	160	simpld 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c e. N )
163		simplrr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> c =/= f )
164	163	necomd 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> f =/= c )
165	107	pmtrprfv 17094	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { f , c } ) ` f ) = c )
167	158, 166	syl5eq 2497	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` f ) = c )
168	155, 167	sylan9eqr 2507	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ a = f ) -> ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) = c )
169	168	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . . . . . . . . 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 3887	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` c ) F b ) )
172	171	adantl 468	. . . . . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . 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 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- a e. _V
176	175	elpr 3986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. { c , f } <-> ( a = c \/ a = f ) )
177	176	notbii 298	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. a e. { c , f } <-> -. ( a = c \/ a = f ) )
178		ioran 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. ( a = c \/ a = f ) <-> ( -. a = c /\ -. a = f ) )
179	177, 178	bitr2i 254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -. a = c /\ -. a = f ) <-> -. a e. { c , f } )
180	179	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -. a = c /\ -. a = f ) -> -. a e. { c , f } )
181	180	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) /\ -. a = c ) /\ -. a = f ) -> -. a e. { c , f } )
182		prssi 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> { c , f } ~~ 2o )
187	107	pmtrmvd 17097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> dom ( ( (pmTrsp ` N ) ` { c , f } ) \ _I ) = { c , f } )
189	188	eleq2d 2514	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 296	. . . . . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . . . . . . . . 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 17096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. Fin /\ { c , f } C_ N /\ { c , f } ~~ 2o ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
194	159, 183, 186, 193	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> ( (pmTrsp ` N ) ` { c , f } ) : N --> N )
195		ffn 5728	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( c e. N /\ f e. N ) /\ c =/= f ) ) /\ a e. N ) -> a e. N )
198		fnelnfp 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) )
200	196, 197, 199	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> if ( a = f , ( ( d ` c ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
206	205	adantl 468	. . . . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . . . . 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 3890	. . . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . . 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 1028	. . . . . . . . . . . . . . . 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 6355	. . . . . . . . . . . . . . 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 474	. . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = c -> ( d ` a ) = ( d ` c ) )
218	217	oveq1d 6305	. . . . . . . . . . . . . . . . . . . 20 |- ( a = c -> ( ( d ` a ) F b ) = ( ( d ` c ) F b ) )
219		iftrue 3887	. . . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = f -> ( d ` a ) = ( d ` f ) )
222	221	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> ( ( d ` a ) F b ) = ( ( d ` f ) F b ) )
223		iftrue 3887	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` f ) F b ) )
224	222, 223	eqtr4d 2488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
225	224	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -. a = c /\ a = f ) -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
226		iffalse 3890	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. a = f -> if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) = ( ( d ` a ) F b ) )
227	226	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. a = f -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
228	227	adantl 468	. . . . . . . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a = c -> ( ( d ` a ) F b ) = if ( a = f , ( ( d ` f ) F b ) , ( ( d ` a ) F b ) ) )
230		iffalse 3890	. . . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . . 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 168	. . . . . . . . . . . . . . . . . 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 6356	. . . . . . . . . . . . . . . 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 5868	. . . . . . . . . . . . . . 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 5868	. . . . . . . . . . . . . 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 2495	. . . . . . . . . . . 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 5864	. . . . . . . . . . . . . . . . 17 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( e ` a ) = ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) )
240	239	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( d ` ( e ` a ) ) = ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) )
241	240	oveq1d 6305	. . . . . . . . . . . . . . 15 |- ( e = ( (pmTrsp ` N ) ` { c , f } ) -> ( ( d ` ( e ` a ) ) F b ) = ( ( d ` ( ( (pmTrsp ` N ) ` { c , f } ) ` a ) ) F b ) )
242	241	mpt2eq3dv 6357	. . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . 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 2453	. . . . . . . . . . . 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 226	. . . . . . . . . . 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 620	. . . . . . . . . 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 433	. . . . . . . . 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 2886	. . . . . . . 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 33	. . . . . . 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 1205	. . . . . 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 1302	. . . . 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 2485	. . . 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 467	. . 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 5865	. . . 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 468	. . 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 2451	. . . . . 6 |- ( invg ` R ) = ( invg ` R )
257	47	3ad2ant1 1029	. . . . . 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 1029	. . . . . . . . 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 1029	. . . . . . . 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 17729	. . . . . . . . 9 |- K = ( Base ` (mulGrp ` R ) )
261	31, 260	mhmf 16587	. . . . . . . 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 6023	. . . . . 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 1029	. . . . . . 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 1040	. . . . . . 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 6023	. . . . . 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 17824	. . . . 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 17727	. . . . . . . . 9 |- .x. = ( +g ` (mulGrp ` R ) )
269	31, 30, 268	mhmlin 16589	. . . . . . . 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 1268	. . . . . . 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 1029	. . . . . . . . 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 1010	. . . . . . . . . 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 19165	. . . . . . . . . 10 |- ( ( N e. Fin /\ e e. ran (pmTrsp ` N ) ) -> e e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
274	271, 272, 273	syl2anc 667	. . . . . . . . 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 2451	. . . . . . . . . 10 |- ( ZRHom ` R ) = ( ZRHom ` R )
276		eqid 2451	. . . . . . . . . 10 |- (pmSgn ` N ) = (pmSgn ` N )
277	275, 276, 54, 31, 256	zrhpsgnodpm 19160	. . . . . . . . 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 1268	. . . . . . . 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 6306	. . . . . . 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 17823	. . . . . . 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 2490	. . . . . 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 6305	. . . . 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 2487	. . . 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 467	. . 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 2489	. 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 1009	. . 3 |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> E : N -1-1-onto-> N )
287	34, 31	elsymgbas 17023	. . . 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 236	. 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 16613	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 188   \/ wo 370   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   A.wral 2737   E.wrex 2738   \ cdif 3401   C_ wss 3404   ifcif 3881   {csn 3968   {cpr 3970   class class class wbr 4402   _I cid 4744   X. cxp 4832   dom cdm 4834   ran crn 4835   |` cres 4836   o. ccom 4838   Fn wfn 5577   -->wf 5578   -1-1-onto->wf1o 5581   ` cfv 5582  (class class class)co 6290   |-> cmpt2 6292   oFcof 6529   2oc2o 7176   ^m cmap 7472   ~~ cen 7566   Fincfn 7569   Basecbs 15121   +g cplusg 15190   .rcmulr 15191   0gc0g 15338  mrClscmrc 15489   Mndcmnd 16535   MndHom cmhm 16580  SubMndcsubmnd 16581   Grpcgrp 16669   invgcminusg 16670   SymGrpcsymg 17018  pmTrspcpmtr 17082  pmSgncpsgn 17130  pmEvencevpm 17131  mulGrpcmgp 17723   1rcur 17735   Ringcrg 17780   ZRHomczrh 19071   Mat cmat 19432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598