Theorem mdetralt 20781

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	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetralt.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetralt.b	⊢ 𝐵 = (Base‘𝐴)
mdetralt.z	⊢ 0 = (0g‘𝑅)
mdetralt.r	⊢ (𝜑 → 𝑅 ∈ CRing)
mdetralt.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mdetralt.i	⊢ (𝜑 → 𝐼 ∈ 𝑁)
mdetralt.j	⊢ (𝜑 → 𝐽 ∈ 𝑁)
mdetralt.ij	⊢ (𝜑 → 𝐼 ≠ 𝐽)
mdetralt.eq	⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))

Assertion

Ref	Expression
mdetralt	⊢ (𝜑 → (𝐷‘𝑋) = 0 )

Distinct variable groups:   𝐼,𝑎   𝐽,𝑎   𝑁,𝑎   𝑋,𝑎

Allowed substitution hints:   𝜑(𝑎)   𝐴(𝑎)   𝐵(𝑎)   𝐷(𝑎)   𝑅(𝑎)   0 (𝑎)

Proof of Theorem mdetralt

Dummy variables 𝑐 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdetralt.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
2		mdetralt.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
3		mdetralt.a	. . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅)
4		mdetralt.b	. . . 4 ⊢ 𝐵 = (Base‘𝐴)
5		eqid 2824	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
6		eqid 2824	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
7		eqid 2824	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
8		eqid 2824	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
9		eqid 2824	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	mdetleib 20760	. . 3 ⊢ (𝑋 ∈ 𝐵 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
11	1, 10	syl 17	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
12		eqid 2824	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
13		eqid 2824	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
14		mdetralt.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
15		crngring 18911	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
16	14, 15	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
17		ringcmn 18934	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ CMnd)
19	3, 4	matrcl 20584	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
21	20	simpld 490	. . . 4 ⊢ (𝜑 → 𝑁 ∈ Fin)
22		eqid 2824	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
23	22, 5	symgbasfi 18155	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
24	21, 23	syl 17	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
25	16	adantr 474	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
26		zrhpsgnmhm 20288	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
27	16, 21, 26	syl2anc 581	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
28	9, 12	mgpbas 18848	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
29	5, 28	mhmf 17692	. . . . . 6 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
30	27, 29	syl 17	. . . . 5 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
31	30	ffvelrnda 6607	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
32	9	crngmgp 18908	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
33	14, 32	syl 17	. . . . . 6 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
34	33	adantr 474	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
35	21	adantr 474	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
36	3, 12, 4	matbas2i 20594	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
37	1, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
38		elmapi 8143	. . . . . . . . 9 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
39	37, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
40	39	ad2antrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
41	22, 5	symgbasf1o 18152	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
42	41	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
43		f1of 6377	. . . . . . . . 9 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
45	44	ffvelrnda 6607	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
46		simpr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
47	40, 45, 46	fovrnd 7065	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
48	47	ralrimiva 3174	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
49	28, 34, 35, 48	gsummptcl 18718	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
50	12, 8	ringcl 18914	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
51	25, 31, 49, 50	syl3anc 1496	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
52		disjdif 4262	. . . 4 ⊢ ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅
53	52	a1i 11	. . 3 ⊢ (𝜑 → ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅)
54	22, 5	evpmss 20290	. . . . . 6 ⊢ (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
55		undif 4271	. . . . . 6 ⊢ ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)))
56	54, 55	mpbi 222	. . . . 5 ⊢ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁))
57	56	eqcomi 2833	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
58	57	a1i 11	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
59		eqid 2824	. . 3 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
60	12, 13, 18, 24, 51, 53, 58, 59	gsummptfidmsplitres 18683	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g‘𝑅)(𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))))
61		resmpt 5685	. . . . . . 7 ⊢ ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
62	54, 61	ax-mp 5	. . . . . 6 ⊢ ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
63	16	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring)
64	21	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin)
65		simpr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁))
66		eqid 2824	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
67	6, 7, 66	zrhpsgnevpm 20295	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
68	63, 64, 65, 67	syl3anc 1496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
69	68	oveq1d 6919	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
70	54	sseli 3822	. . . . . . . . . 10 ⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
71	70, 49	sylan2 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
72	12, 8, 66	ringlidm 18924	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
73	63, 71, 72	syl2anc 581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
74	69, 73	eqtrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
75	74	mpteq2dva 4966	. . . . . 6 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
76	62, 75	syl5eq 2872	. . . . 5 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
77	76	oveq2d 6920	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
78		difss 3963	. . . . . . . 8 ⊢ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))
79		resmpt 5685	. . . . . . . 8 ⊢ (((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
81	16	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring)
82	21	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin)
83		simpr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
84		eqid 2824	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
85	6, 7, 66, 5, 84	zrhpsgnodpm 20296	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
86	81, 82, 83, 85	syl3anc 1496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
87	86	oveq1d 6919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
88		eldifi 3958	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
89	88, 49	sylan2 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
90	12, 8, 66, 84, 81, 89	ringnegl 18947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
91	87, 90	eqtrd 2860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
92	91	mpteq2dva 4966	. . . . . . . 8 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
93		eqidd 2825	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
94		ringgrp 18905	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
95	16, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Grp)
96	12, 84	grpinvf 17819	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Grp → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
97	95, 96	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
98	97	feqmptd 6495	. . . . . . . . 9 ⊢ (𝜑 → (invg‘𝑅) = (𝑞 ∈ (Base‘𝑅) ↦ ((invg‘𝑅)‘𝑞)))
99		fveq2 6432	. . . . . . . . 9 ⊢ (𝑞 = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) → ((invg‘𝑅)‘𝑞) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
100	89, 93, 98, 99	fmptco 6645	. . . . . . . 8 ⊢ (𝜑 → ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
101	92, 100	eqtr4d 2863	. . . . . . 7 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
102	80, 101	syl5eq 2872	. . . . . 6 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
103	102	oveq2d 6920	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
104		mdetralt.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
105		ringabl 18933	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
106	16, 105	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Abel)
107		difssd 3964	. . . . . . 7 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)))
108		ssfi 8448	. . . . . . 7 ⊢ (((Base‘(SymGrp‘𝑁)) ∈ Fin ∧ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))) → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
109	24, 107, 108	syl2anc 581	. . . . . 6 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
110		eqid 2824	. . . . . 6 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
111	12, 104, 84, 106, 109, 89, 110	gsummptfidminv 18699	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
112	89	ralrimiva 3174	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
113		mdetralt.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
114		mdetralt.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
115		prssi 4569	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → {𝐼, 𝐽} ⊆ 𝑁)
116	113, 114, 115	syl2anc 581	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁)
117		mdetralt.ij	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
118		pr2nelem 9139	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
119	113, 114, 117, 118	syl3anc 1496	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o)
120		eqid 2824	. . . . . . . . . . . 12 ⊢ (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
121		eqid 2824	. . . . . . . . . . . 12 ⊢ ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
122	120, 121	pmtrrn 18226	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
123	21, 116, 119, 122	syl3anc 1496	. . . . . . . . . 10 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
124	22, 5, 121	pmtrodpm 20302	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
125	21, 123, 124	syl2anc 581	. . . . . . . . 9 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
126	22, 5	evpmodpmf1o 20301	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
127	21, 125, 126	syl2anc 581	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
128	12, 18, 109, 112, 110, 127	gsummptfif1o 18719	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))))
129		eleq1w 2888	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁)))
130	129	anbi2d 624	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁))))
131		oveq2 6912	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))
132	131	eleq1d 2890	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
133	130, 132	imbi12d 336	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))))
134	22	symggrp 18169	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
135	21, 134	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp)
136	135	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp)
137	121, 22, 5	symgtrf 18238	. . . . . . . . . . . . . 14 ⊢ ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
138	123	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
139	137, 138	sseldi 3824	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
140	70	adantl 475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
141		eqid 2824	. . . . . . . . . . . . . 14 ⊢ (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
142	5, 141	grpcl 17783	. . . . . . . . . . . . 13 ⊢ (((SymGrp‘𝑁) ∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
143	136, 139, 140, 142	syl3anc 1496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
144		eqid 2824	. . . . . . . . . . . . . . . . 17 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})
145	22, 7, 144	psgnghm2 20285	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ Fin → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
146	21, 145	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
147	146	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
148		prex 5129	. . . . . . . . . . . . . . . 16 ⊢ {1, -1} ∈ V
149		eqid 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
150		cnfldmul 20111	. . . . . . . . . . . . . . . . . 18 ⊢ · = (.r‘ℂfld)
151	149, 150	mgpplusg 18846	. . . . . . . . . . . . . . . . 17 ⊢ · = (+g‘(mulGrp‘ℂfld))
152	144, 151	ressplusg 16351	. . . . . . . . . . . . . . . 16 ⊢ ({1, -1} ∈ V → · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1})))
153	148, 152	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1}))
154	5, 141, 153	ghmlin 18015	. . . . . . . . . . . . . 14 ⊢ (((pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})) ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
155	147, 139, 140, 154	syl3anc 1496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
156	22, 121, 7	psgnpmtr 18280	. . . . . . . . . . . . . . . 16 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
157	138, 156	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
158	22, 5, 7	psgnevpm 20293	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
159	21, 158	sylan 577	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
160	157, 159	oveq12d 6922	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1))
161		neg1cn 11471	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
162	161	mulid1i 10360	. . . . . . . . . . . . . 14 ⊢ (-1 · 1) = -1
163	160, 162	syl6eq 2876	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1)
164	155, 163	eqtrd 2860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1)
165	22, 5, 7	psgnodpmr 20294	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
166	64, 143, 164, 165	syl3anc 1496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
167	133, 166	chvarv 2416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
168		eqidd 2825	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))
169		fveq1 6431	. . . . . . . . . . . . 13 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐))
170	169	oveq1d 6919	. . . . . . . . . . . 12 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))
171	170	mpteq2dv 4967	. . . . . . . . . . 11 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))
172	171	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))
173	167, 168, 93, 172	fmptco 6645	. . . . . . . . 9 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))))
174		oveq2 6912	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝))
175	174	fveq1d 6434	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐))
176	175	oveq1d 6919	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))
177	176	mpteq2dv 4967	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))
178	177	oveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
179	178	cbvmptv 4972	. . . . . . . . . 10 ⊢ (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
180	179	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))))
181	139	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
182	140	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
183	22, 5, 141	symgov 18159	. . . . . . . . . . . . . . . . 17 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
184	181, 182, 183	syl2anc 581	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
185	184	fveq1d 6434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐))
186	70, 44	sylan2 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁)
187		fvco3 6521	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
188	186, 187	sylan 577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
189	185, 188	eqtrd 2860	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
190	189	oveq1d 6919	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐))
191	120	pmtrprfv 18222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
192	21, 113, 114, 117, 191	syl13anc 1497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
193	192	ad2antrr 719	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
194	193	oveq1d 6919	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐))
195		oveq2 6912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐))
196		oveq2 6912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐))
197	195, 196	eqeq12d 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐)))
198		mdetralt.eq	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
199	198	ad2antrr 719	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
200		simpr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
201	197, 199, 200	rspcdva 3531	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐))
202	194, 201	eqtr4d 2863	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))
203		fveq2 6432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼))
204	203	oveq1d 6919	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐))
205		oveq1 6911	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐))
206	204, 205	eqeq12d 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)))
207	202, 206	syl5ibrcom 239	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
208		prcom 4484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
209	208	fveq2i 6435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼})
210	209	fveq1i 6433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽)
211	117	necomd 3053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
212	120	pmtrprfv 18222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
213	21, 114, 113, 211, 212	syl13anc 1497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
214	210, 213	syl5eq 2872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼)
215	214	oveq1d 6919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
216	215	ad2antrr 719	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
217	216, 201	eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))
218		fveq2 6432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽))
219	218	oveq1d 6919	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐))
220		oveq1 6911	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐))
221	219, 220	eqeq12d 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)))
222	217, 221	syl5ibrcom 239	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
223	222	a1dd 50	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
224		neanior 3090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
225		elpri 4418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽))
226	225	orcomd 904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
227	226	con3i 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
228	224, 227	sylbi 209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
229	228	3adant1 1166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
230	120	pmtrmvd 18225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
231	21, 116, 119, 230	syl3anc 1496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
232	231	ad2antrr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
233	232	3ad2ant1 1169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
234	229, 233	neleqtrrd 2927	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))
235	120	pmtrf 18224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
236	21, 116, 119, 235	syl3anc 1496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
237	236	ffnd 6278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
238	237	ad2antrr 719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
239	186	ffvelrnda 6607	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
240		fnelnfp 6694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
241	238, 239, 240	syl2anc 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
242	241	3ad2ant1 1169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
243	242	necon2bbid 3041	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )))
244	234, 243	mpbird 249	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐))
245	244	oveq1d 6919	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
246	245	3exp 1154	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
247	223, 246	pm2.61dne 3084	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
248	207, 247	pm2.61dne 3084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
249	190, 248	eqtrd 2860	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
250	249	mpteq2dva 4966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))
251	250	oveq2d 6920	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
252	251	mpteq2dva 4966	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
253	173, 180, 252	3eqtrd 2864	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
254	253	oveq2d 6920	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
255	128, 254	eqtrd 2860	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
256	255	fveq2d 6436	. . . . 5 ⊢ (𝜑 → ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
257	103, 111, 256	3eqtrd 2864	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
258	77, 257	oveq12d 6922	. . 3 ⊢ (𝜑 → ((𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g‘𝑅)(𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) = ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))))
259	54	a1i 11	. . . . . 6 ⊢ (𝜑 → (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
260		ssfi 8448	. . . . . 6 ⊢ (((Base‘(SymGrp‘𝑁)) ∈ Fin ∧ (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))) → (pmEven‘𝑁) ∈ Fin)
261	24, 259, 260	syl2anc 581	. . . . 5 ⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin)
262	71	ralrimiva 3174	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
263	12, 18, 261, 262	gsummptcl 18718	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅))
264	12, 13, 104, 84	grprinv 17822	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
265	95, 263, 264	syl2anc 581	. . 3 ⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
266	258, 265	eqtrd 2860	. 2 ⊢ (𝜑 → ((𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g‘𝑅)(𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) = 0 )
267	11, 60, 266	3eqtrd 2864	1 ⊢ (𝜑 → (𝐷‘𝑋) = 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166   ≠ wne 2998  ∀wral 3116  Vcvv 3413   ∖ cdif 3794   ∪ cun 3795   ∩ cin 3796   ⊆ wss 3797  ∅c0 4143  {cpr 4398   class class class wbr 4872   ↦ cmpt 4951   I cid 5248   × cxp 5339  dom cdm 5341  ran crn 5342   ↾ cres 5343   ∘ ccom 5345   Fn wfn 6117  ⟶wf 6118  –1-1-onto→wf1o 6121  ‘cfv 6122  (class class class)co 6904  2_oc2o 7819   ↑_𝑚 cmap 8121   ≈ cen 8218  Fincfn 8221  1c1 10252   · cmul 10256  -cneg 10585  Basecbs 16221   ↾_s cress 16222  +_gcplusg 16304  ._rcmulr 16305  0_gc0g 16452   Σ_g cgsu 16453   MndHom cmhm 17685  Grpcgrp 17775  inv_gcminusg 17776   GrpHom cghm 18007  SymGrpcsymg 18146  pmTrspcpmtr 18210  pmSgncpsgn 18258  pmEvencevpm 18259  CMndccmn 18545  Abelcabl 18546  mulGrpcmgp 18842  1_rcur 18854  Ringcrg 18900  CRingccrg 18901  ℂ_fldccnfld 20105  ℤRHomczrh 20207   Mat cmat 20579   maDet cmdat 20757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-inf2 8814  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-addf 10330  ax-mulf 10331

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-xor 1640  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-ot 4405  df-uni 4658  df-int 4697  df-iun 4741  df-iin 4742  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-se 5301  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-isom 6131  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-of 7156  df-om 7326  df-1st 7427  df-2nd 7428  df-supp 7559  df-tpos 7616  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-oadd 7829  df-er 8008  df-map 8123  df-pm 8124  df-ixp 8175  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-fsupp 8544  df-sup 8616  df-oi 8683  df-card 9077  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-4 11415  df-5 11416  df-6 11417  df-7 11418  df-8 11419  df-9 11420  df-n0 11618  df-xnn0 11690  df-z 11704  df-dec 11821  df-uz 11968  df-rp 12112  df-fz 12619  df-fzo 12760  df-seq 13095  df-exp 13154  df-hash 13410  df-word 13574  df-lsw 13622  df-concat 13630  df-s1 13655  df-substr 13700  df-pfx 13749  df-splice 13856  df-reverse 13874  df-s2 13968  df-struct 16223  df-ndx 16224  df-slot 16225  df-base 16227  df-sets 16228  df-ress 16229  df-plusg 16317  df-mulr 16318  df-starv 16319  df-sca 16320  df-vsca 16321  df-ip 16322  df-tset 16323  df-ple 16324  df-ds 16326  df-unif 16327  df-hom 16328  df-cco 16329  df-0g 16454  df-gsum 16455  df-prds 16460  df-pws 16462  df-mre 16598  df-mrc 16599  df-acs 16601  df-mgm 17594  df-sgrp 17636  df-mnd 17647  df-mhm 17687  df-submnd 17688  df-grp 17778  df-minusg 17779  df-mulg 17894  df-subg 17941  df-ghm 18008  df-gim 18051  df-cntz 18099  df-oppg 18125  df-symg 18147  df-pmtr 18211  df-psgn 18260  df-evpm 18261  df-cmn 18547  df-abl 18548  df-mgp 18843  df-ur 18855  df-ring 18902  df-cring 18903  df-oppr 18976  df-dvdsr 18994  df-unit 18995  df-invr 19025  df-dvr 19036  df-rnghom 19070  df-drng 19104  df-subrg 19133  df-sra 19532  df-rgmod 19533  df-cnfld 20106  df-zring 20178  df-zrh 20211  df-dsmm 20438  df-frlm 20453  df-mat 20580  df-mdet 20758

This theorem is referenced by:  mdetralt2  20782  mdetuni0  20794  mdetmul  20796