Theorem mdetralt 19214

Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 23-Jul-2018.)

Hypotheses

Ref	Expression
mdetralt.d	|- D = ( N maDet R )
mdetralt.a	|- A = ( N Mat R )
mdetralt.b	|- B = ( Base ` A )
mdetralt.z	|- .0. = ( 0g ` R )
mdetralt.r	|- ( ph -> R e. CRing )
mdetralt.x	|- ( ph -> X e. B )
mdetralt.i	|- ( ph -> I e. N )
mdetralt.j	|- ( ph -> J e. N )
mdetralt.ij	|- ( ph -> I =/= J )
mdetralt.eq	|- ( ph -> A. a e. N ( I X a ) = ( J X a ) )

Assertion

Ref	Expression
mdetralt	|- ( ph -> ( D ` X ) = .0. )

Distinct variable groups:   I, a   J, a   N, a   X, a

Allowed substitution hints:   ph( a)   A( a)   B( a)   D( a)   R( a)   .0. ( a)

Proof of Theorem mdetralt

Dummy variables c p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdetralt.x	. . 3 |- ( ph -> X e. B )
2		mdetralt.d	. . . 4 |- D = ( N maDet R )
3		mdetralt.a	. . . 4 |- A = ( N Mat R )
4		mdetralt.b	. . . 4 |- B = ( Base ` A )
5		eqid 2392	. . . 4 |- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
6		eqid 2392	. . . 4 |- ( ZRHom ` R ) = ( ZRHom ` R )
7		eqid 2392	. . . 4 |- (pmSgn ` N ) = (pmSgn ` N )
8		eqid 2392	. . . 4 |- ( .r ` R ) = ( .r ` R )
9		eqid 2392	. . . 4 |- (mulGrp ` R ) = (mulGrp ` R )
10	2, 3, 4, 5, 6, 7, 8, 9	mdetleib 19193	. . 3 |- ( X e. B -> ( D ` X ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
11	1, 10	syl 16	. 2 |- ( ph -> ( D ` X ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
12		eqid 2392	. . 3 |- ( Base ` R ) = ( Base ` R )
13		eqid 2392	. . 3 |- ( +g ` R ) = ( +g ` R )
14		mdetralt.r	. . . . 5 |- ( ph -> R e. CRing )
15		crngring 17341	. . . . 5 |- ( R e. CRing -> R e. Ring )
16	14, 15	syl 16	. . . 4 |- ( ph -> R e. Ring )
17		ringcmn 17361	. . . 4 |- ( R e. Ring -> R e. CMnd )
18	16, 17	syl 16	. . 3 |- ( ph -> R e. CMnd )
19	3, 4	matrcl 19018	. . . . . 6 |- ( X e. B -> ( N e. Fin /\ R e. _V ) )
20	1, 19	syl 16	. . . . 5 |- ( ph -> ( N e. Fin /\ R e. _V ) )
21	20	simpld 457	. . . 4 |- ( ph -> N e. Fin )
22		eqid 2392	. . . . 5 |- ( SymGrp ` N ) = ( SymGrp ` N )
23	22, 5	symgbasfi 16547	. . . 4 |- ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )
24	21, 23	syl 16	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) e. Fin )
25	16	adantr 463	. . . 4 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )
26		zrhpsgnmhm 18730	. . . . . . 7 |- ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
27	16, 21, 26	syl2anc 659	. . . . . 6 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) )
28	9, 12	mgpbas 17279	. . . . . . 7 |- ( Base ` R ) = ( Base ` (mulGrp ` R ) )
29	5, 28	mhmf 16107	. . . . . 6 |- ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom (mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> ( Base ` R ) )
30	27, 29	syl 16	. . . . 5 |- ( ph -> ( ( ZRHom ` R ) o. (pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> ( Base ` R ) )
31	30	ffvelrnda 5946	. . . 4 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) e. ( Base ` R ) )
32	9	crngmgp 17338	. . . . . . 7 |- ( R e. CRing -> (mulGrp ` R ) e. CMnd )
33	14, 32	syl 16	. . . . . 6 |- ( ph -> (mulGrp ` R ) e. CMnd )
34	33	adantr 463	. . . . 5 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> (mulGrp ` R ) e. CMnd )
35	21	adantr 463	. . . . 5 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N e. Fin )
36	3, 12, 4	matbas2i 19028	. . . . . . . . . 10 |- ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
37	1, 36	syl 16	. . . . . . . . 9 |- ( ph -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
38		elmapi 7377	. . . . . . . . 9 |- ( X e. ( ( Base ` R ) ^m ( N X. N ) ) -> X : ( N X. N ) --> ( Base ` R ) )
39	37, 38	syl 16	. . . . . . . 8 |- ( ph -> X : ( N X. N ) --> ( Base ` R ) )
40	39	ad2antrr 723	. . . . . . 7 |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> X : ( N X. N ) --> ( Base ` R ) )
41	22, 5	symgbasf1o 16544	. . . . . . . . . 10 |- ( p e. ( Base ` ( SymGrp ` N ) ) -> p : N -1-1-onto-> N )
42	41	adantl 464	. . . . . . . . 9 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N -1-1-onto-> N )
43		f1of 5737	. . . . . . . . 9 |- ( p : N -1-1-onto-> N -> p : N --> N )
44	42, 43	syl 16	. . . . . . . 8 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N --> N )
45	44	ffvelrnda 5946	. . . . . . 7 |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> ( p ` c ) e. N )
46		simpr 459	. . . . . . 7 |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> c e. N )
47	40, 45, 46	fovrnd 6364	. . . . . 6 |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> ( ( p ` c ) X c ) e. ( Base ` R ) )
48	47	ralrimiva 2806	. . . . 5 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. c e. N ( ( p ` c ) X c ) e. ( Base ` R ) )
49	28, 34, 35, 48	gsummptcl 17127	. . . 4 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) )
50	12, 8	ringcl 17344	. . . 4 |- ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) e. ( Base ` R ) /\ ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) e. ( Base ` R ) )
51	25, 31, 49, 50	syl3anc 1226	. . 3 |- ( ( ph /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) e. ( Base ` R ) )
52		disjdif 3829	. . . 4 |- ( (pmEven ` N ) i^i ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = (/)
53	52	a1i 11	. . 3 |- ( ph -> ( (pmEven ` N ) i^i ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = (/) )
54	22, 5	evpmss 18732	. . . . . 6 |- (pmEven ` N ) C_ ( Base ` ( SymGrp ` N ) )
55		undif 3837	. . . . . 6 |- ( (pmEven ` N ) C_ ( Base ` ( SymGrp ` N ) ) <-> ( (pmEven ` N ) u. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = ( Base ` ( SymGrp ` N ) ) )
56	54, 55	mpbi 208	. . . . 5 |- ( (pmEven ` N ) u. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = ( Base ` ( SymGrp ` N ) )
57	56	eqcomi 2405	. . . 4 |- ( Base ` ( SymGrp ` N ) ) = ( (pmEven ` N ) u. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
58	57	a1i 11	. . 3 |- ( ph -> ( Base ` ( SymGrp ` N ) ) = ( (pmEven ` N ) u. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) )
59		eqid 2392	. . 3 |- ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
60	12, 13, 18, 24, 51, 53, 58, 59	gsummptfidmsplitres 17086	. 2 |- ( ph -> ( R gsumg ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) = ( ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) ) ( +g ` R ) ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) ) )
61		resmpt 5248	. . . . . . 7 |- ( (pmEven ` N ) C_ ( Base ` ( SymGrp ` N ) ) -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) = ( p e. (pmEven ` N ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
62	54, 61	ax-mp 5	. . . . . 6 |- ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) = ( p e. (pmEven ` N ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
63	16	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ p e. (pmEven ` N ) ) -> R e. Ring )
64	21	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ p e. (pmEven ` N ) ) -> N e. Fin )
65		simpr 459	. . . . . . . . . 10 |- ( ( ph /\ p e. (pmEven ` N ) ) -> p e. (pmEven ` N ) )
66		eqid 2392	. . . . . . . . . . 11 |- ( 1r ` R ) = ( 1r ` R )
67	6, 7, 66	zrhpsgnevpm 18737	. . . . . . . . . 10 |- ( ( R e. Ring /\ N e. Fin /\ p e. (pmEven ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) = ( 1r ` R ) )
68	63, 64, 65, 67	syl3anc 1226	. . . . . . . . 9 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) = ( 1r ` R ) )
69	68	oveq1d 6229	. . . . . . . 8 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( ( 1r ` R ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
70	54	sseli 3426	. . . . . . . . . 10 |- ( p e. (pmEven ` N ) -> p e. ( Base ` ( SymGrp ` N ) ) )
71	70, 49	sylan2 472	. . . . . . . . 9 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) )
72	12, 8, 66	ringlidm 17354	. . . . . . . . 9 |- ( ( R e. Ring /\ ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) )
73	63, 71, 72	syl2anc 659	. . . . . . . 8 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( 1r ` R ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) )
74	69, 73	eqtrd 2433	. . . . . . 7 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) )
75	74	mpteq2dva 4466	. . . . . 6 |- ( ph -> ( p e. (pmEven ` N ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
76	62, 75	syl5eq 2445	. . . . 5 |- ( ph -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
77	76	oveq2d 6230	. . . 4 |- ( ph -> ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) ) = ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
78		difss 3558	. . . . . . . 8 |- ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) C_ ( Base ` ( SymGrp ` N ) )
79		resmpt 5248	. . . . . . . 8 |- ( ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) C_ ( Base ` ( SymGrp ` N ) ) -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
80	78, 79	ax-mp 5	. . . . . . 7 |- ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
81	16	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> R e. Ring )
82	21	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> N e. Fin )
83		simpr 459	. . . . . . . . . . . 12 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
84		eqid 2392	. . . . . . . . . . . . 13 |- ( invg ` R ) = ( invg ` R )
85	6, 7, 66, 5, 84	zrhpsgnodpm 18738	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ N e. Fin /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
86	81, 82, 83, 85	syl3anc 1226	. . . . . . . . . . 11 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
87	86	oveq1d 6229	. . . . . . . . . 10 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
88		eldifi 3553	. . . . . . . . . . . 12 |- ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) -> p e. ( Base ` ( SymGrp ` N ) ) )
89	88, 49	sylan2 472	. . . . . . . . . . 11 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) )
90	12, 8, 66, 84, 81, 89	ringnegl 17372	. . . . . . . . . 10 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( ( invg ` R ) ` ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
91	87, 90	eqtrd 2433	. . . . . . . . 9 |- ( ( ph /\ p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( ( invg ` R ) ` ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
92	91	mpteq2dva 4466	. . . . . . . 8 |- ( ph -> ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( invg ` R ) ` ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
93		eqidd 2393	. . . . . . . . 9 |- ( ph -> ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
94		ringgrp 17335	. . . . . . . . . . . 12 |- ( R e. Ring -> R e. Grp )
95	16, 94	syl 16	. . . . . . . . . . 11 |- ( ph -> R e. Grp )
96	12, 84	grpinvf 16230	. . . . . . . . . . 11 |- ( R e. Grp -> ( invg ` R ) : ( Base ` R ) --> ( Base ` R ) )
97	95, 96	syl 16	. . . . . . . . . 10 |- ( ph -> ( invg ` R ) : ( Base ` R ) --> ( Base ` R ) )
98	97	feqmptd 5840	. . . . . . . . 9 |- ( ph -> ( invg ` R ) = ( q e. ( Base ` R ) |-> ( ( invg ` R ) ` q ) ) )
99		fveq2 5787	. . . . . . . . 9 |- ( q = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) -> ( ( invg ` R ) ` q ) = ( ( invg ` R ) ` ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
100	89, 93, 98, 99	fmptco 5979	. . . . . . . 8 |- ( ph -> ( ( invg ` R ) o. ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( invg ` R ) ` ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
101	92, 100	eqtr4d 2436	. . . . . . 7 |- ( ph -> ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( ( invg ` R ) o. ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
102	80, 101	syl5eq 2445	. . . . . 6 |- ( ph -> ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) = ( ( invg ` R ) o. ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
103	102	oveq2d 6230	. . . . 5 |- ( ph -> ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) = ( R gsumg ( ( invg ` R ) o. ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
104		mdetralt.z	. . . . . 6 |- .0. = ( 0g ` R )
105		ringabl 17360	. . . . . . 7 |- ( R e. Ring -> R e. Abel )
106	16, 105	syl 16	. . . . . 6 |- ( ph -> R e. Abel )
107		difssd 3559	. . . . . . 7 |- ( ph -> ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) C_ ( Base ` ( SymGrp ` N ) ) )
108		ssfi 7674	. . . . . . 7 |- ( ( ( Base ` ( SymGrp ` N ) ) e. Fin /\ ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) C_ ( Base ` ( SymGrp ` N ) ) ) -> ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) e. Fin )
109	24, 107, 108	syl2anc 659	. . . . . 6 |- ( ph -> ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) e. Fin )
110		eqid 2392	. . . . . 6 |- ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) = ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) )
111	12, 104, 84, 106, 109, 89, 110	gsummptfidminv 17107	. . . . 5 |- ( ph -> ( R gsumg ( ( invg ` R ) o. ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) = ( ( invg ` R ) ` ( R gsumg ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
112	89	ralrimiva 2806	. . . . . . . 8 |- ( ph -> A. p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) )
113		mdetralt.i	. . . . . . . . . . . 12 |- ( ph -> I e. N )
114		mdetralt.j	. . . . . . . . . . . 12 |- ( ph -> J e. N )
115		prssi 4113	. . . . . . . . . . . 12 |- ( ( I e. N /\ J e. N ) -> { I , J } C_ N )
116	113, 114, 115	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> { I , J } C_ N )
117		mdetralt.ij	. . . . . . . . . . . 12 |- ( ph -> I =/= J )
118		pr2nelem 8313	. . . . . . . . . . . 12 |- ( ( I e. N /\ J e. N /\ I =/= J ) -> { I , J } ~~ 2o )
119	113, 114, 117, 118	syl3anc 1226	. . . . . . . . . . 11 |- ( ph -> { I , J } ~~ 2o )
120		eqid 2392	. . . . . . . . . . . 12 |- (pmTrsp ` N ) = (pmTrsp ` N )
121		eqid 2392	. . . . . . . . . . . 12 |- ran (pmTrsp ` N ) = ran (pmTrsp ` N )
122	120, 121	pmtrrn 16618	. . . . . . . . . . 11 |- ( ( N e. Fin /\ { I , J } C_ N /\ { I , J } ~~ 2o ) -> ( (pmTrsp ` N ) ` { I , J } ) e. ran (pmTrsp ` N ) )
123	21, 116, 119, 122	syl3anc 1226	. . . . . . . . . 10 |- ( ph -> ( (pmTrsp ` N ) ` { I , J } ) e. ran (pmTrsp ` N ) )
124	22, 5, 121	pmtrodpm 18743	. . . . . . . . . 10 |- ( ( N e. Fin /\ ( (pmTrsp ` N ) ` { I , J } ) e. ran (pmTrsp ` N ) ) -> ( (pmTrsp ` N ) ` { I , J } ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
125	21, 123, 124	syl2anc 659	. . . . . . . . 9 |- ( ph -> ( (pmTrsp ` N ) ` { I , J } ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
126	22, 5	evpmodpmf1o 18742	. . . . . . . . 9 |- ( ( N e. Fin /\ ( (pmTrsp ` N ) ` { I , J } ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) -> ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) : (pmEven ` N ) -1-1-onto-> ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
127	21, 125, 126	syl2anc 659	. . . . . . . 8 |- ( ph -> ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) : (pmEven ` N ) -1-1-onto-> ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
128	12, 18, 109, 112, 110, 127	gsummptfif1o 17128	. . . . . . 7 |- ( ph -> ( R gsumg ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( R gsumg ( ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) o. ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) ) ) )
129		eleq1 2464	. . . . . . . . . . . . 13 |- ( p = q -> ( p e. (pmEven ` N ) <-> q e. (pmEven ` N ) ) )
130	129	anbi2d 701	. . . . . . . . . . . 12 |- ( p = q -> ( ( ph /\ p e. (pmEven ` N ) ) <-> ( ph /\ q e. (pmEven ` N ) ) ) )
131		oveq2 6222	. . . . . . . . . . . . 13 |- ( p = q -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) )
132	131	eleq1d 2461	. . . . . . . . . . . 12 |- ( p = q -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) <-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) )
133	130, 132	imbi12d 318	. . . . . . . . . . 11 |- ( p = q -> ( ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) <-> ( ( ph /\ q e. (pmEven ` N ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) )
134	22	symggrp 16561	. . . . . . . . . . . . . . 15 |- ( N e. Fin -> ( SymGrp ` N ) e. Grp )
135	21, 134	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( SymGrp ` N ) e. Grp )
136	135	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( SymGrp ` N ) e. Grp )
137	121, 22, 5	symgtrf 16630	. . . . . . . . . . . . . 14 |- ran (pmTrsp ` N ) C_ ( Base ` ( SymGrp ` N ) )
138	123	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmTrsp ` N ) ` { I , J } ) e. ran (pmTrsp ` N ) )
139	137, 138	sseldi 3428	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmTrsp ` N ) ` { I , J } ) e. ( Base ` ( SymGrp ` N ) ) )
140	70	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. (pmEven ` N ) ) -> p e. ( Base ` ( SymGrp ` N ) ) )
141		eqid 2392	. . . . . . . . . . . . . 14 |- ( +g ` ( SymGrp ` N ) ) = ( +g ` ( SymGrp ` N ) )
142	5, 141	grpcl 16199	. . . . . . . . . . . . 13 |- ( ( ( SymGrp ` N ) e. Grp /\ ( (pmTrsp ` N ) ` { I , J } ) e. ( Base ` ( SymGrp ` N ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( Base ` ( SymGrp ` N ) ) )
143	136, 139, 140, 142	syl3anc 1226	. . . . . . . . . . . 12 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( Base ` ( SymGrp ` N ) ) )
144		eqid 2392	. . . . . . . . . . . . . . . . 17 |- ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) = ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } )
145	22, 7, 144	psgnghm2 18727	. . . . . . . . . . . . . . . 16 |- ( N e. Fin -> (pmSgn ` N ) e. ( ( SymGrp ` N ) GrpHom ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) ) )
146	21, 145	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> (pmSgn ` N ) e. ( ( SymGrp ` N ) GrpHom ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) ) )
147	146	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. (pmEven ` N ) ) -> (pmSgn ` N ) e. ( ( SymGrp ` N ) GrpHom ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) ) )
148		prex 4617	. . . . . . . . . . . . . . . 16 |- { 1 , -u 1 } e. _V
149		eqid 2392	. . . . . . . . . . . . . . . . . 18 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
150		cnfldmul 18558	. . . . . . . . . . . . . . . . . 18 |- x. = ( .r ` ℂfld )
151	149, 150	mgpplusg 17277	. . . . . . . . . . . . . . . . 17 |- x. = ( +g ` (mulGrp ` ℂfld ) )
152	144, 151	ressplusg 14767	. . . . . . . . . . . . . . . 16 |- ( { 1 , -u 1 } e. _V -> x. = ( +g ` ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) ) )
153	148, 152	ax-mp 5	. . . . . . . . . . . . . . 15 |- x. = ( +g ` ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) )
154	5, 141, 153	ghmlin 16408	. . . . . . . . . . . . . 14 |- ( ( (pmSgn ` N ) e. ( ( SymGrp ` N ) GrpHom ( (mulGrp ` ℂfld ) ↾s { 1 , -u 1 } ) ) /\ ( (pmTrsp ` N ) ` { I , J } ) e. ( Base ` ( SymGrp ` N ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( (pmSgn ` N ) ` ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ) = ( ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) x. ( (pmSgn ` N ) ` p ) ) )
155	147, 139, 140, 154	syl3anc 1226	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmSgn ` N ) ` ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ) = ( ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) x. ( (pmSgn ` N ) ` p ) ) )
156	22, 121, 7	psgnpmtr 16671	. . . . . . . . . . . . . . . 16 |- ( ( (pmTrsp ` N ) ` { I , J } ) e. ran (pmTrsp ` N ) -> ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) = -u 1 )
157	138, 156	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) = -u 1 )
158	22, 5, 7	psgnevpm 18735	. . . . . . . . . . . . . . . 16 |- ( ( N e. Fin /\ p e. (pmEven ` N ) ) -> ( (pmSgn ` N ) ` p ) = 1 )
159	21, 158	sylan 469	. . . . . . . . . . . . . . 15 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmSgn ` N ) ` p ) = 1 )
160	157, 159	oveq12d 6232	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) x. ( (pmSgn ` N ) ` p ) ) = ( -u 1 x. 1 ) )
161		neg1cn 10574	. . . . . . . . . . . . . . 15 |- -u 1 e. CC
162	161	mulid1i 9527	. . . . . . . . . . . . . 14 |- ( -u 1 x. 1 ) = -u 1
163	160, 162	syl6eq 2449	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( (pmSgn ` N ) ` ( (pmTrsp ` N ) ` { I , J } ) ) x. ( (pmSgn ` N ) ` p ) ) = -u 1 )
164	155, 163	eqtrd 2433	. . . . . . . . . . . 12 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (pmSgn ` N ) ` ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ) = -u 1 )
165	22, 5, 7	psgnodpmr 18736	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( Base ` ( SymGrp ` N ) ) /\ ( (pmSgn ` N ) ` ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ) = -u 1 ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
166	64, 143, 164, 165	syl3anc 1226	. . . . . . . . . . 11 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
167	133, 166	chvarv 2031	. . . . . . . . . 10 |- ( ( ph /\ q e. (pmEven ` N ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) )
168		eqidd 2393	. . . . . . . . . 10 |- ( ph -> ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) = ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) )
169		fveq1 5786	. . . . . . . . . . . . 13 |- ( p = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) -> ( p ` c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) )
170	169	oveq1d 6229	. . . . . . . . . . . 12 |- ( p = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) -> ( ( p ` c ) X c ) = ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) )
171	170	mpteq2dv 4467	. . . . . . . . . . 11 |- ( p = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) -> ( c e. N |-> ( ( p ` c ) X c ) ) = ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) )
172	171	oveq2d 6230	. . . . . . . . . 10 |- ( p = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) ) )
173	167, 168, 93, 172	fmptco 5979	. . . . . . . . 9 |- ( ph -> ( ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) o. ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) ) = ( q e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) ) ) )
174		oveq2 6222	. . . . . . . . . . . . . . 15 |- ( q = p -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) = ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) )
175	174	fveq1d 5789	. . . . . . . . . . . . . 14 |- ( q = p -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) )
176	175	oveq1d 6229	. . . . . . . . . . . . 13 |- ( q = p -> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) = ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) )
177	176	mpteq2dv 4467	. . . . . . . . . . . 12 |- ( q = p -> ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) = ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) )
178	177	oveq2d 6230	. . . . . . . . . . 11 |- ( q = p -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) ) )
179	178	cbvmptv 4471	. . . . . . . . . 10 |- ( q e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) ) )
180	179	a1i 11	. . . . . . . . 9 |- ( ph -> ( q e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ` c ) X c ) ) ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) ) ) )
181	139	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( (pmTrsp ` N ) ` { I , J } ) e. ( Base ` ( SymGrp ` N ) ) )
182	140	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> p e. ( Base ` ( SymGrp ` N ) ) )
183	22, 5, 141	symgov 16551	. . . . . . . . . . . . . . . . 17 |- ( ( ( (pmTrsp ` N ) ` { I , J } ) e. ( Base ` ( SymGrp ` N ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) = ( ( (pmTrsp ` N ) ` { I , J } ) o. p ) )
184	181, 182, 183	syl2anc 659	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) = ( ( (pmTrsp ` N ) ` { I , J } ) o. p ) )
185	184	fveq1d 5789	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) o. p ) ` c ) )
186	70, 44	sylan2 472	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. (pmEven ` N ) ) -> p : N --> N )
187		fvco3 5864	. . . . . . . . . . . . . . . 16 |- ( ( p : N --> N /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) o. p ) ` c ) = ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) )
188	186, 187	sylan 469	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) o. p ) ` c ) = ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) )
189	185, 188	eqtrd 2433	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) = ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) )
190	189	oveq1d 6229	. . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) )
191	120	pmtrprfv 16614	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. Fin /\ ( I e. N /\ J e. N /\ I =/= J ) ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) = J )
192	21, 113, 114, 117, 191	syl13anc 1228	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) = J )
193	192	ad2antrr 723	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) = J )
194	193	oveq1d 6229	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) X c ) = ( J X c ) )
195		simpr 459	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> c e. N )
196		mdetralt.eq	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. a e. N ( I X a ) = ( J X a ) )
197	196	ad2antrr 723	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> A. a e. N ( I X a ) = ( J X a ) )
198		oveq2 6222	. . . . . . . . . . . . . . . . . . 19 |- ( a = c -> ( I X a ) = ( I X c ) )
199		oveq2 6222	. . . . . . . . . . . . . . . . . . 19 |- ( a = c -> ( J X a ) = ( J X c ) )
200	198, 199	eqeq12d 2414	. . . . . . . . . . . . . . . . . 18 |- ( a = c -> ( ( I X a ) = ( J X a ) <-> ( I X c ) = ( J X c ) ) )
201	200	rspcv 3144	. . . . . . . . . . . . . . . . 17 |- ( c e. N -> ( A. a e. N ( I X a ) = ( J X a ) -> ( I X c ) = ( J X c ) ) )
202	195, 197, 201	sylc 60	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( I X c ) = ( J X c ) )
203	194, 202	eqtr4d 2436	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) X c ) = ( I X c ) )
204		fveq2 5787	. . . . . . . . . . . . . . . . 17 |- ( ( p ` c ) = I -> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) = ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) )
205	204	oveq1d 6229	. . . . . . . . . . . . . . . 16 |- ( ( p ` c ) = I -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) X c ) )
206		oveq1 6221	. . . . . . . . . . . . . . . 16 |- ( ( p ` c ) = I -> ( ( p ` c ) X c ) = ( I X c ) )
207	205, 206	eqeq12d 2414	. . . . . . . . . . . . . . 15 |- ( ( p ` c ) = I -> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) <-> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` I ) X c ) = ( I X c ) ) )
208	203, 207	syl5ibrcom 222	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) = I -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) ) )
209		prcom 4035	. . . . . . . . . . . . . . . . . . . . . . 23 |- { I , J } = { J , I }
210	209	fveq2i 5790	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (pmTrsp ` N ) ` { I , J } ) = ( (pmTrsp ` N ) ` { J , I } )
211	210	fveq1i 5788	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) = ( ( (pmTrsp ` N ) ` { J , I } ) ` J )
212	117	necomd 2663	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> J =/= I )
213	120	pmtrprfv 16614	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ ( J e. N /\ I e. N /\ J =/= I ) ) -> ( ( (pmTrsp ` N ) ` { J , I } ) ` J ) = I )
214	21, 114, 113, 212, 213	syl13anc 1228	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( (pmTrsp ` N ) ` { J , I } ) ` J ) = I )
215	211, 214	syl5eq 2445	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) = I )
216	215	oveq1d 6229	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) X c ) = ( I X c ) )
217	216	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) X c ) = ( I X c ) )
218	217, 202	eqtrd 2433	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) X c ) = ( J X c ) )
219		fveq2 5787	. . . . . . . . . . . . . . . . . . 19 |- ( ( p ` c ) = J -> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) = ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) )
220	219	oveq1d 6229	. . . . . . . . . . . . . . . . . 18 |- ( ( p ` c ) = J -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) X c ) )
221		oveq1 6221	. . . . . . . . . . . . . . . . . 18 |- ( ( p ` c ) = J -> ( ( p ` c ) X c ) = ( J X c ) )
222	220, 221	eqeq12d 2414	. . . . . . . . . . . . . . . . 17 |- ( ( p ` c ) = J -> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) <-> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` J ) X c ) = ( J X c ) ) )
223	218, 222	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) = J -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) ) )
224	223	a1dd 46	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) = J -> ( ( p ` c ) =/= I -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) ) ) )
225		neanior 2717	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( p ` c ) =/= J /\ ( p ` c ) =/= I ) <-> -. ( ( p ` c ) = J \/ ( p ` c ) = I ) )
226		elpri 3977	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p ` c ) e. { I , J } -> ( ( p ` c ) = I \/ ( p ` c ) = J ) )
227	226	orcomd 386	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p ` c ) e. { I , J } -> ( ( p ` c ) = J \/ ( p ` c ) = I ) )
228	227	con3i 135	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( ( p ` c ) = J \/ ( p ` c ) = I ) -> -. ( p ` c ) e. { I , J } )
229	225, 228	sylbi 195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> -. ( p ` c ) e. { I , J } )
230	229	3adant1 1012	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> -. ( p ` c ) e. { I , J } )
231	120	pmtrmvd 16617	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. Fin /\ { I , J } C_ N /\ { I , J } ~~ 2o ) -> dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) = { I , J } )
232	21, 116, 119, 231	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) = { I , J } )
233	232	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) = { I , J } )
234	233	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) = { I , J } )
235	230, 234	neleqtrrd 2505	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> -. ( p ` c ) e. dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) )
236	120	pmtrf 16616	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( N e. Fin /\ { I , J } C_ N /\ { I , J } ~~ 2o ) -> ( (pmTrsp ` N ) ` { I , J } ) : N --> N )
237	21, 116, 119, 236	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( (pmTrsp ` N ) ` { I , J } ) : N --> N )
238		ffn 5652	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( (pmTrsp ` N ) ` { I , J } ) : N --> N -> ( (pmTrsp ` N ) ` { I , J } ) Fn N )
239	237, 238	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( (pmTrsp ` N ) ` { I , J } ) Fn N )
240	239	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( (pmTrsp ` N ) ` { I , J } ) Fn N )
241	186	ffvelrnda 5946	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( p ` c ) e. N )
242		fnelnfp 6017	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( (pmTrsp ` N ) ` { I , J } ) Fn N /\ ( p ` c ) e. N ) -> ( ( p ` c ) e. dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) =/= ( p ` c ) ) )
243	240, 241, 242	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) e. dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) =/= ( p ` c ) ) )
244	243	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> ( ( p ` c ) e. dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) <-> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) =/= ( p ` c ) ) )
245	244	necon2bbid 2648	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) = ( p ` c ) <-> -. ( p ` c ) e. dom ( ( (pmTrsp ` N ) ` { I , J } ) \ _I ) ) )
246	235, 245	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) = ( p ` c ) )
247	246	oveq1d 6229	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) /\ ( p ` c ) =/= J /\ ( p ` c ) =/= I ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) )
248	247	3exp 1193	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) =/= J -> ( ( p ` c ) =/= I -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) ) ) )
249	224, 248	pm2.61dne 2709	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( p ` c ) =/= I -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) ) )
250	208, 249	pm2.61dne 2709	. . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( (pmTrsp ` N ) ` { I , J } ) ` ( p ` c ) ) X c ) = ( ( p ` c ) X c ) )
251	190, 250	eqtrd 2433	. . . . . . . . . . . 12 |- ( ( ( ph /\ p e. (pmEven ` N ) ) /\ c e. N ) -> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) = ( ( p ` c ) X c ) )
252	251	mpteq2dva 4466	. . . . . . . . . . 11 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) = ( c e. N |-> ( ( p ` c ) X c ) ) )
253	252	oveq2d 6230	. . . . . . . . . 10 |- ( ( ph /\ p e. (pmEven ` N ) ) -> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) ) = ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) )
254	253	mpteq2dva 4466	. . . . . . . . 9 |- ( ph -> ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) p ) ` c ) X c ) ) ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
255	173, 180, 254	3eqtrd 2437	. . . . . . . 8 |- ( ph -> ( ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) o. ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) ) = ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) )
256	255	oveq2d 6230	. . . . . . 7 |- ( ph -> ( R gsumg ( ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) o. ( q e. (pmEven ` N ) |-> ( ( (pmTrsp ` N ) ` { I , J } ) ( +g ` ( SymGrp ` N ) ) q ) ) ) ) = ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
257	128, 256	eqtrd 2433	. . . . . 6 |- ( ph -> ( R gsumg ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) = ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) )
258	257	fveq2d 5791	. . . . 5 |- ( ph -> ( ( invg ` R ) ` ( R gsumg ( p e. ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) = ( ( invg ` R ) ` ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
259	103, 111, 258	3eqtrd 2437	. . . 4 |- ( ph -> ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) = ( ( invg ` R ) ` ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) )
260	77, 259	oveq12d 6232	. . 3 |- ( ph -> ( ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) ) ( +g ` R ) ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) ) = ( ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ( +g ` R ) ( ( invg ` R ) ` ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) ) )
261	54	a1i 11	. . . . . 6 |- ( ph -> (pmEven ` N ) C_ ( Base ` ( SymGrp ` N ) ) )
262		ssfi 7674	. . . . . 6 |- ( ( ( Base ` ( SymGrp ` N ) ) e. Fin /\ (pmEven ` N ) C_ ( Base ` ( SymGrp ` N ) ) ) -> (pmEven ` N ) e. Fin )
263	24, 261, 262	syl2anc 659	. . . . 5 |- ( ph -> (pmEven ` N ) e. Fin )
264	71	ralrimiva 2806	. . . . 5 |- ( ph -> A. p e. (pmEven ` N ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) e. ( Base ` R ) )
265	12, 18, 263, 264	gsummptcl 17127	. . . 4 |- ( ph -> ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) e. ( Base ` R ) )
266	12, 13, 104, 84	grprinv 16233	. . . 4 |- ( ( R e. Grp /\ ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) e. ( Base ` R ) ) -> ( ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ( +g ` R ) ( ( invg ` R ) ` ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) ) = .0. )
267	95, 265, 266	syl2anc 659	. . 3 |- ( ph -> ( ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ( +g ` R ) ( ( invg ` R ) ` ( R gsumg ( p e. (pmEven ` N ) |-> ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) ) ) = .0. )
268	260, 267	eqtrd 2433	. 2 |- ( ph -> ( ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` (pmEven ` N ) ) ) ( +g ` R ) ( R gsumg ( ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( c e. N |-> ( ( p ` c ) X c ) ) ) ) ) |` ( ( Base ` ( SymGrp ` N ) ) \ (pmEven ` N ) ) ) ) ) = .0. )
269	11, 60, 268	3eqtrd 2437	1 |- ( ph -> ( D ` X ) = .0. )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 366   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1836   =/= wne 2587   A.wral 2742   _Vcvv 3047   \ cdif 3399   u. cun 3400   i^i cin 3401   C_ wss 3402   (/)c0 3724   {cpr 3959   class class class wbr 4380   |-> cmpt 4438   _I cid 4717   X. cxp 4924   dom cdm 4926   ran crn 4927   |` cres 4928   o. ccom 4930   Fn wfn 5504   -->wf 5505   -1-1-onto->wf1o 5508   ` cfv 5509  (class class class)co 6214   2oc2o 7060   ^m cmap 7356   ~~ cen 7450   Fincfn 7453   1c1 9422   x. cmul 9426   -ucneg 9737   Basecbs 14653   ↾_s cress 14654   +g cplusg 14721   .rcmulr 14722   0gc0g 14866   gsum_g cgsu 14867   MndHom cmhm 16100   Grpcgrp 16189   invgcminusg 16190   GrpHom cghm 16400   SymGrpcsymg 16538  pmTrspcpmtr 16602  pmSgncpsgn 16650  pmEvencevpm 16651  CMndccmn 16934   Abelcabl 16935  mulGrpcmgp 17273   1rcur 17285   Ringcrg 17330   CRingccrg 17331  ℂ_fldccnfld 18552   ZRHomczrh 18649   Mat cmat 19013   maDet cmdat 19190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-inf2 7990  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498  ax-addf 9500  ax-mulf 9501

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-xor 1363  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-ot 3966  df-uni 4177  df-int 4213  df-iun 4258  df-iin 4259  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-se 4766  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-isom 5518  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-of 6457  df-om 6618  df-1st 6717  df-2nd 6718  df-supp 6836  df-tpos 6891  df-recs 6978  df-rdg 7012  df-1o 7066  df-2o 7067  df-oadd 7070  df-er 7247  df-map 7358  df-pm 7359  df-ixp 7407  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-fsupp 7763  df-sup 7834  df-oi 7868  df-card 8251  df-cda 8479  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142  df-nn 10471  df-2 10529  df-3 10530  df-4 10531  df-5 10532  df-6 10533  df-7 10534  df-8 10535  df-9 10536  df-10 10537  df-n0 10731  df-z 10800  df-dec 10914  df-uz 11020  df-rp 11158  df-fz 11612  df-fzo 11736  df-seq 12030  df-exp 12089  df-hash 12327  df-word 12465  df-lsw 12466  df-concat 12467  df-s1 12468  df-substr 12469  df-splice 12470  df-reverse 12471  df-s2 12743  df-struct 14655  df-ndx 14656  df-slot 14657  df-base 14658  df-sets 14659  df-ress 14660  df-plusg 14734  df-mulr 14735  df-starv 14736  df-sca 14737  df-vsca 14738  df-ip 14739  df-tset 14740  df-ple 14741  df-ds 14743  df-unif 14744  df-hom 14745  df-cco 14746  df-0g 14868  df-gsum 14869  df-prds 14874  df-pws 14876  df-mre 15012  df-mrc 15013  df-acs 15015  df-mgm 16008  df-sgrp 16047  df-mnd 16057  df-mhm 16102  df-submnd 16103  df-grp 16193  df-minusg 16194  df-mulg 16196  df-subg 16334  df-ghm 16401  df-gim 16443  df-cntz 16491  df-oppg 16517  df-symg 16539  df-pmtr 16603  df-psgn 16652  df-evpm 16653  df-cmn 16936  df-abl 16937  df-mgp 17274  df-ur 17286  df-ring 17332  df-cring 17333  df-oppr 17404  df-dvdsr 17422  df-unit 17423  df-invr 17453  df-dvr 17464  df-rnghom 17496  df-drng 17530  df-subrg 17559  df-sra 17950  df-rgmod 17951  df-cnfld 18553  df-zring 18621  df-zrh 18653  df-dsmm 18873  df-frlm 18888  df-mat 19014  df-mdet 19191

This theorem is referenced by:  mdetralt2  19215  mdetuni0  19227  mdetmul  19229