Theorem mdetralt 22493

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 2729	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
6		eqid 2729	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
7		eqid 2729	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
8		eqid 2729	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
9		eqid 2729	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	mdetleib 22472	. . 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 2729	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
13		eqid 2729	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
14		mdetralt.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
15		crngring 20130	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
16	14, 15	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
17		ringcmn 20167	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ CMnd)
19	3, 4	matrcl 22297	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
21	20	simpld 494	. . . 4 ⊢ (𝜑 → 𝑁 ∈ Fin)
22		eqid 2729	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
23	22, 5	symgbasfi 19258	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
24	21, 23	syl 17	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
25	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
26		zrhpsgnmhm 21491	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
27	16, 21, 26	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
28	9, 12	mgpbas 20030	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
29	5, 28	mhmf 18663	. . . . . 6 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
30	27, 29	syl 17	. . . . 5 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
31	30	ffvelcdmda 7018	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
32	9	crngmgp 20126	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
33	14, 32	syl 17	. . . . . 6 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
34	33	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
35	21	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
36	3, 12, 4	matbas2i 22307	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
37	1, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
38		elmapi 8776	. . . . . . . . 9 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
39	37, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
40	39	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
41	22, 5	symgbasf1o 19254	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
42	41	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
43		f1of 6764	. . . . . . . . 9 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
45	44	ffvelcdmda 7018	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
46		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
47	40, 45, 46	fovcdmd 7521	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
48	47	ralrimiva 3121	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
49	28, 34, 35, 48	gsummptcl 19846	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
50	12, 8	ringcl 20135	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
51	25, 31, 49, 50	syl3anc 1373	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
52		disjdif 4423	. . . 4 ⊢ ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅
53	52	a1i 11	. . 3 ⊢ (𝜑 → ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅)
54	22, 5	evpmss 21493	. . . . . 6 ⊢ (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
55		undif 4433	. . . . . 6 ⊢ ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)))
56	54, 55	mpbi 230	. . . . 5 ⊢ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁))
57	56	eqcomi 2738	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
58	57	a1i 11	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
59		eqid 2729	. . 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 19810	. 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 5988	. . . . . . 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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring)
64	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin)
65		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁))
66		eqid 2729	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
67	6, 7, 66	zrhpsgnevpm 21498	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
68	63, 64, 65, 67	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
69	68	oveq1d 7364	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
70	54	sseli 3931	. . . . . . . . . 10 ⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
71	70, 49	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
72	12, 8, 66	ringlidm 20154	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
73	63, 71, 72	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
74	69, 73	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
75	74	mpteq2dva 5185	. . . . . 6 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
76	62, 75	eqtrid 2776	. . . . 5 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
77	76	oveq2d 7365	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
78		difss 4087	. . . . . . . 8 ⊢ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))
79		resmpt 5988	. . . . . . . 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 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring)
82	21	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin)
83		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
84		eqid 2729	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
85	6, 7, 66, 5, 84	zrhpsgnodpm 21499	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
86	81, 82, 83, 85	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
87	86	oveq1d 7364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
88		eldifi 4082	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
89	88, 49	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
90	12, 8, 66, 84, 81, 89	ringnegl 20187	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
91	87, 90	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
92	91	mpteq2dva 5185	. . . . . . . 8 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
93		ringgrp 20123	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
94	16, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Grp)
95	12, 84	grpinvf 18865	. . . . . . . . . 10 ⊢ (𝑅 ∈ Grp → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
96	94, 95	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
97	96, 89	cofmpt 7066	. . . . . . . 8 ⊢ (𝜑 → ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
98	92, 97	eqtr4d 2767	. . . . . . 7 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
99	80, 98	eqtrid 2776	. . . . . 6 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
100	99	oveq2d 7365	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
101		mdetralt.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
102		ringabl 20166	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
103	16, 102	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Abel)
104		difssd 4088	. . . . . . 7 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)))
105	24, 104	ssfid 9158	. . . . . 6 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
106		eqid 2729	. . . . . 6 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
107	12, 101, 84, 103, 105, 89, 106	gsummptfidminv 19826	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
108	89	ralrimiva 3121	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
109		mdetralt.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
110		mdetralt.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
111	109, 110	prssd 4773	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁)
112		mdetralt.ij	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
113		enpr2 9898	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
114	109, 110, 112, 113	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o)
115		eqid 2729	. . . . . . . . . . . 12 ⊢ (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
116		eqid 2729	. . . . . . . . . . . 12 ⊢ ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
117	115, 116	pmtrrn 19336	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
118	21, 111, 114, 117	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
119	22, 5, 116	pmtrodpm 21504	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
120	21, 118, 119	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
121	22, 5	evpmodpmf1o 21503	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
122	21, 120, 121	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
123	12, 18, 105, 108, 106, 122	gsummptfif1o 19847	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))))
124		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁)))
125	124	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁))))
126		oveq2 7357	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))
127	126	eleq1d 2813	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
128	125, 127	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))))
129	22	symggrp 19279	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
130	21, 129	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp)
131	130	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp)
132	116, 22, 5	symgtrf 19348	. . . . . . . . . . . . . 14 ⊢ ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
133	118	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
134	132, 133	sselid 3933	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
135	70	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
136		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
137	5, 136	grpcl 18820	. . . . . . . . . . . . 13 ⊢ (((SymGrp‘𝑁) ∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
138	131, 134, 135, 137	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
139		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})
140	22, 7, 139	psgnghm2 21488	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ Fin → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
141	21, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
142	141	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
143		prex 5376	. . . . . . . . . . . . . . . 16 ⊢ {1, -1} ∈ V
144		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
145		cnfldmul 21269	. . . . . . . . . . . . . . . . . 18 ⊢ · = (.r‘ℂfld)
146	144, 145	mgpplusg 20029	. . . . . . . . . . . . . . . . 17 ⊢ · = (+g‘(mulGrp‘ℂfld))
147	139, 146	ressplusg 17195	. . . . . . . . . . . . . . . 16 ⊢ ({1, -1} ∈ V → · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1})))
148	143, 147	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1}))
149	5, 136, 148	ghmlin 19100	. . . . . . . . . . . . . 14 ⊢ (((pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})) ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
150	142, 134, 135, 149	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
151	22, 116, 7	psgnpmtr 19389	. . . . . . . . . . . . . . . 16 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
152	133, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
153	22, 5, 7	psgnevpm 21496	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
154	21, 153	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
155	152, 154	oveq12d 7367	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1))
156		neg1cn 12113	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
157	156	mulridi 11119	. . . . . . . . . . . . . 14 ⊢ (-1 · 1) = -1
158	155, 157	eqtrdi 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1)
159	150, 158	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1)
160	22, 5, 7	psgnodpmr 21497	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
161	64, 138, 159, 160	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
162	128, 161	chvarvv 1989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
163		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))
164		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
165		fveq1 6821	. . . . . . . . . . . . 13 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐))
166	165	oveq1d 7364	. . . . . . . . . . . 12 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))
167	166	mpteq2dv 5186	. . . . . . . . . . 11 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))
168	167	oveq2d 7365	. . . . . . . . . 10 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))
169	162, 163, 164, 168	fmptco 7063	. . . . . . . . 9 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))))
170		oveq2 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝))
171	170	fveq1d 6824	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐))
172	171	oveq1d 7364	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))
173	172	mpteq2dv 5186	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))
174	173	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
175	174	cbvmptv 5196	. . . . . . . . . 10 ⊢ (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
176	175	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))))
177	134	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
178	135	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
179	22, 5, 136	symgov 19263	. . . . . . . . . . . . . . . . 17 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
180	177, 178, 179	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
181	180	fveq1d 6824	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐))
182	70, 44	sylan2 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁)
183		fvco3 6922	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
184	182, 183	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
185	181, 184	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
186	185	oveq1d 7364	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐))
187	115	pmtrprfv 19332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
188	21, 109, 110, 112, 187	syl13anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
189	188	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
190	189	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐))
191		oveq2 7357	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐))
192		oveq2 7357	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐))
193	191, 192	eqeq12d 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐)))
194		mdetralt.eq	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
195	194	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
196		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
197	193, 195, 196	rspcdva 3578	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐))
198	190, 197	eqtr4d 2767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))
199		fveq2 6822	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼))
200	199	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐))
201		oveq1 7356	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐))
202	200, 201	eqeq12d 2745	. . . . . . . . . . . . . . 15 ⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)))
203	198, 202	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
204		prcom 4684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
205	204	fveq2i 6825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼})
206	205	fveq1i 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽)
207	112	necomd 2980	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
208	115	pmtrprfv 19332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
209	21, 110, 109, 207, 208	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
210	206, 209	eqtrid 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼)
211	210	oveq1d 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
212	211	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
213	212, 197	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))
214		fveq2 6822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽))
215	214	oveq1d 7364	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐))
216		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐))
217	215, 216	eqeq12d 2745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)))
218	213, 217	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
219	218	a1dd 50	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
220		neanior 3018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
221		elpri 4601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽))
222	221	orcomd 871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
223	222	con3i 154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
224	220, 223	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
225	224	3adant1 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
226	115	pmtrmvd 19335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
227	21, 111, 114, 226	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
228	227	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
229	228	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
230	225, 229	neleqtrrd 2851	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))
231	115	pmtrf 19334	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
232	21, 111, 114, 231	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
233	232	ffnd 6653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
234	233	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
235	182	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
236		fnelnfp 7113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
237	234, 235, 236	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
238	237	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
239	238	necon2bbid 2968	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )))
240	230, 239	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐))
241	240	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
242	241	3exp 1119	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
243	219, 242	pm2.61dne 3011	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
244	203, 243	pm2.61dne 3011	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
245	186, 244	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
246	245	mpteq2dva 5185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))
247	246	oveq2d 7365	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
248	247	mpteq2dva 5185	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
249	169, 176, 248	3eqtrd 2768	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
250	249	oveq2d 7365	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
251	123, 250	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
252	251	fveq2d 6826	. . . . 5 ⊢ (𝜑 → ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
253	100, 107, 252	3eqtrd 2768	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
254	77, 253	oveq12d 7367	. . 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 (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))))
255	54	a1i 11	. . . . . 6 ⊢ (𝜑 → (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
256	24, 255	ssfid 9158	. . . . 5 ⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin)
257	71	ralrimiva 3121	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
258	12, 18, 256, 257	gsummptcl 19846	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅))
259	12, 13, 101, 84	grprinv 18869	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
260	94, 258, 259	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
261	254, 260	eqtrd 2764	. 2 ⊢ (𝜑 → ((𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g‘𝑅)(𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) = 0 )
262	11, 60, 261	3eqtrd 2768	1 ⊢ (𝜑 → (𝐷‘𝑋) = 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3436   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4284  {cpr 4579   class class class wbr 5092   ↦ cmpt 5173   I cid 5513   × cxp 5617  dom cdm 5619  ran crn 5620   ↾ cres 5621   ∘ ccom 5623   Fn wfn 6477  ⟶wf 6478  –1-1-onto→wf1o 6481  ‘cfv 6482  (class class class)co 7349  2_oc2o 8382   ↑_m cmap 8753   ≈ cen 8869  Fincfn 8872  1c1 11010   · cmul 11014  -cneg 11348  Basecbs 17120   ↾_s cress 17141  +_gcplusg 17161  ._rcmulr 17162  0_gc0g 17343   Σ_g cgsu 17344   MndHom cmhm 18655  Grpcgrp 18812  inv_gcminusg 18813   GrpHom cghm 19091  SymGrpcsymg 19248  pmTrspcpmtr 19320  pmSgncpsgn 19368  pmEvencevpm 19369  CMndccmn 19659  Abelcabl 19660  mulGrpcmgp 20025  1_rcur 20066  Ringcrg 20118  CRingccrg 20119  ℂ_fldccnfld 21261  ℤRHomczrh 21406   Mat cmat 22292   maDet cmdat 22469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-addf 11088  ax-mulf 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-ot 4586  df-uni 4859  df-int 4897  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7613  df-om 7800  df-1st 7924  df-2nd 7925  df-supp 8094  df-tpos 8159  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-er 8625  df-map 8755  df-pm 8756  df-ixp 8825  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-fsupp 9252  df-sup 9332  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198  df-n0 12385  df-xnn0 12458  df-z 12472  df-dec 12592  df-uz 12736  df-rp 12894  df-fz 13411  df-fzo 13558  df-seq 13909  df-exp 13969  df-hash 14238  df-word 14421  df-lsw 14470  df-concat 14478  df-s1 14503  df-substr 14548  df-pfx 14578  df-splice 14656  df-reverse 14665  df-s2 14755  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-starv 17176  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-unif 17184  df-hom 17185  df-cco 17186  df-0g 17345  df-gsum 17346  df-prds 17351  df-pws 17353  df-mre 17488  df-mrc 17489  df-acs 17491  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-mhm 18657  df-submnd 18658  df-efmnd 18743  df-grp 18815  df-minusg 18816  df-mulg 18947  df-subg 19002  df-ghm 19092  df-gim 19138  df-cntz 19196  df-oppg 19225  df-symg 19249  df-pmtr 19321  df-psgn 19370  df-evpm 19371  df-cmn 19661  df-abl 19662  df-mgp 20026  df-rng 20038  df-ur 20067  df-ring 20120  df-cring 20121  df-oppr 20222  df-dvdsr 20242  df-unit 20243  df-invr 20273  df-dvr 20286  df-rhm 20357  df-subrng 20431  df-subrg 20455  df-drng 20616  df-sra 21077  df-rgmod 21078  df-cnfld 21262  df-zring 21354  df-zrh 21410  df-dsmm 21639  df-frlm 21654  df-mat 22293  df-mdet 22470

This theorem is referenced by:  mdetralt2  22494  mdetuni0  22506  mdetmul  22508