Theorem mdetralt 21309

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 2759	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
6		eqid 2759	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
7		eqid 2759	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
8		eqid 2759	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
9		eqid 2759	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	mdetleib 21288	. . 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 2759	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
13		eqid 2759	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
14		mdetralt.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
15		crngring 19378	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
16	14, 15	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
17		ringcmn 19403	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ CMnd)
19	3, 4	matrcl 21113	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
21	20	simpld 499	. . . 4 ⊢ (𝜑 → 𝑁 ∈ Fin)
22		eqid 2759	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
23	22, 5	symgbasfi 18575	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
24	21, 23	syl 17	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
25	16	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
26		zrhpsgnmhm 20350	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
27	16, 21, 26	syl2anc 588	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
28	9, 12	mgpbas 19314	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
29	5, 28	mhmf 18028	. . . . . 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 6843	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
32	9	crngmgp 19374	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
33	14, 32	syl 17	. . . . . 6 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
34	33	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
35	21	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
36	3, 12, 4	matbas2i 21123	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
37	1, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
38		elmapi 8439	. . . . . . . . 9 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
39	37, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
40	39	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
41	22, 5	symgbasf1o 18571	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
42	41	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
43		f1of 6603	. . . . . . . . 9 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
45	44	ffvelrnda 6843	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
46		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
47	40, 45, 46	fovrnd 7317	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
48	47	ralrimiva 3114	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
49	28, 34, 35, 48	gsummptcl 19156	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
50	12, 8	ringcl 19383	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
51	25, 31, 49, 50	syl3anc 1369	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
52		disjdif 4369	. . . 4 ⊢ ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅
53	52	a1i 11	. . 3 ⊢ (𝜑 → ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅)
54	22, 5	evpmss 20352	. . . . . 6 ⊢ (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
55		undif 4379	. . . . . 6 ⊢ ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)))
56	54, 55	mpbi 233	. . . . 5 ⊢ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁))
57	56	eqcomi 2768	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
58	57	a1i 11	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
59		eqid 2759	. . 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 19120	. 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 5878	. . . . . . 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 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring)
64	21	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin)
65		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁))
66		eqid 2759	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
67	6, 7, 66	zrhpsgnevpm 20357	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
68	63, 64, 65, 67	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
69	68	oveq1d 7166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
70	54	sseli 3889	. . . . . . . . . 10 ⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
71	70, 49	sylan2 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
72	12, 8, 66	ringlidm 19393	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
73	63, 71, 72	syl2anc 588	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
74	69, 73	eqtrd 2794	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
75	74	mpteq2dva 5128	. . . . . 6 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
76	62, 75	syl5eq 2806	. . . . 5 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
77	76	oveq2d 7167	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
78		difss 4038	. . . . . . . 8 ⊢ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))
79		resmpt 5878	. . . . . . . 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 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring)
82	21	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin)
83		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
84		eqid 2759	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
85	6, 7, 66, 5, 84	zrhpsgnodpm 20358	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
86	81, 82, 83, 85	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
87	86	oveq1d 7166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
88		eldifi 4033	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
89	88, 49	sylan2 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
90	12, 8, 66, 84, 81, 89	ringnegl 19416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
91	87, 90	eqtrd 2794	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
92	91	mpteq2dva 5128	. . . . . . . 8 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
93		ringgrp 19371	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
94	16, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Grp)
95	12, 84	grpinvf 18218	. . . . . . . . . 10 ⊢ (𝑅 ∈ Grp → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
96	94, 95	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
97	96, 89	cofmpt 6886	. . . . . . . 8 ⊢ (𝜑 → ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
98	92, 97	eqtr4d 2797	. . . . . . 7 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
99	80, 98	syl5eq 2806	. . . . . 6 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
100	99	oveq2d 7167	. . . . 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 19402	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
103	16, 102	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Abel)
104		difssd 4039	. . . . . . 7 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)))
105	24, 104	ssfid 8779	. . . . . 6 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
106		eqid 2759	. . . . . 6 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
107	12, 101, 84, 103, 105, 89, 106	gsummptfidminv 19136	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
108	89	ralrimiva 3114	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
109		mdetralt.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
110		mdetralt.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
111	109, 110	prssd 4713	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁)
112		mdetralt.ij	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
113		pr2nelem 9465	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
114	109, 110, 112, 113	syl3anc 1369	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o)
115		eqid 2759	. . . . . . . . . . . 12 ⊢ (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
116		eqid 2759	. . . . . . . . . . . 12 ⊢ ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
117	115, 116	pmtrrn 18653	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
118	21, 111, 114, 117	syl3anc 1369	. . . . . . . . . 10 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
119	22, 5, 116	pmtrodpm 20363	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
120	21, 118, 119	syl2anc 588	. . . . . . . . 9 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
121	22, 5	evpmodpmf1o 20362	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
122	21, 120, 121	syl2anc 588	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
123	12, 18, 105, 108, 106, 122	gsummptfif1o 19157	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))))
124		eleq1w 2835	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁)))
125	124	anbi2d 632	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁))))
126		oveq2 7159	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))
127	126	eleq1d 2837	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
128	125, 127	imbi12d 349	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))))
129	22	symggrp 18596	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
130	21, 129	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp)
131	130	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp)
132	116, 22, 5	symgtrf 18665	. . . . . . . . . . . . . 14 ⊢ ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
133	118	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
134	132, 133	sseldi 3891	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
135	70	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
136		eqid 2759	. . . . . . . . . . . . . 14 ⊢ (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
137	5, 136	grpcl 18178	. . . . . . . . . . . . 13 ⊢ (((SymGrp‘𝑁) ∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
138	131, 134, 135, 137	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
139		eqid 2759	. . . . . . . . . . . . . . . . 17 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})
140	22, 7, 139	psgnghm2 20347	. . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
143		prex 5302	. . . . . . . . . . . . . . . 16 ⊢ {1, -1} ∈ V
144		eqid 2759	. . . . . . . . . . . . . . . . . 18 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
145		cnfldmul 20173	. . . . . . . . . . . . . . . . . 18 ⊢ · = (.r‘ℂfld)
146	144, 145	mgpplusg 19312	. . . . . . . . . . . . . . . . 17 ⊢ · = (+g‘(mulGrp‘ℂfld))
147	139, 146	ressplusg 16671	. . . . . . . . . . . . . . . 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 18431	. . . . . . . . . . . . . 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 1369	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
151	22, 116, 7	psgnpmtr 18706	. . . . . . . . . . . . . . . 16 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
152	133, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
153	22, 5, 7	psgnevpm 20355	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
154	21, 153	sylan 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
155	152, 154	oveq12d 7169	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1))
156		neg1cn 11789	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
157	156	mulid1i 10684	. . . . . . . . . . . . . 14 ⊢ (-1 · 1) = -1
158	155, 157	eqtrdi 2810	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1)
159	150, 158	eqtrd 2794	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1)
160	22, 5, 7	psgnodpmr 20356	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
161	64, 138, 159, 160	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
162	128, 161	chvarvv 2006	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
163		eqidd 2760	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))
164		eqidd 2760	. . . . . . . . . 10 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
165		fveq1 6658	. . . . . . . . . . . . 13 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐))
166	165	oveq1d 7166	. . . . . . . . . . . 12 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))
167	166	mpteq2dv 5129	. . . . . . . . . . 11 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))
168	167	oveq2d 7167	. . . . . . . . . 10 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))
169	162, 163, 164, 168	fmptco 6883	. . . . . . . . 9 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))))
170		oveq2 7159	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝))
171	170	fveq1d 6661	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐))
172	171	oveq1d 7166	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))
173	172	mpteq2dv 5129	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))
174	173	oveq2d 7167	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
175	174	cbvmptv 5136	. . . . . . . . . 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 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
178	135	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
179	22, 5, 136	symgov 18580	. . . . . . . . . . . . . . . . 17 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
180	177, 178, 179	syl2anc 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
181	180	fveq1d 6661	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐))
182	70, 44	sylan2 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁)
183		fvco3 6752	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
184	182, 183	sylan 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
185	181, 184	eqtrd 2794	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
186	185	oveq1d 7166	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐))
187	115	pmtrprfv 18649	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
188	21, 109, 110, 112, 187	syl13anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
189	188	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
190	189	oveq1d 7166	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐))
191		oveq2 7159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐))
192		oveq2 7159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐))
193	191, 192	eqeq12d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐)))
194		mdetralt.eq	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
195	194	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
196		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
197	193, 195, 196	rspcdva 3544	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐))
198	190, 197	eqtr4d 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))
199		fveq2 6659	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼))
200	199	oveq1d 7166	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐))
201		oveq1 7158	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐))
202	200, 201	eqeq12d 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)))
203	198, 202	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
204		prcom 4626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
205	204	fveq2i 6662	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼})
206	205	fveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽)
207	112	necomd 3007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
208	115	pmtrprfv 18649	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
209	21, 110, 109, 207, 208	syl13anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
210	206, 209	syl5eq 2806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼)
211	210	oveq1d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
212	211	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
213	212, 197	eqtrd 2794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))
214		fveq2 6659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽))
215	214	oveq1d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐))
216		oveq1 7158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐))
217	215, 216	eqeq12d 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)))
218	213, 217	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
219	218	a1dd 50	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
220		neanior 3044	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
221		elpri 4545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽))
222	221	orcomd 869	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
223	222	con3i 157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
224	220, 223	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
225	224	3adant1 1128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
226	115	pmtrmvd 18652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
227	21, 111, 114, 226	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
228	227	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
229	228	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
230	225, 229	neleqtrrd 2875	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))
231	115	pmtrf 18651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
232	21, 111, 114, 231	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
233	232	ffnd 6500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
234	233	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
235	182	ffvelrnda 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
236		fnelnfp 6931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
237	234, 235, 236	syl2anc 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
238	237	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
239	238	necon2bbid 2995	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )))
240	230, 239	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐))
241	240	oveq1d 7166	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
242	241	3exp 1117	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
243	219, 242	pm2.61dne 3038	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
244	203, 243	pm2.61dne 3038	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
245	186, 244	eqtrd 2794	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
246	245	mpteq2dva 5128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))
247	246	oveq2d 7167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
248	247	mpteq2dva 5128	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
249	169, 176, 248	3eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
250	249	oveq2d 7167	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
251	123, 250	eqtrd 2794	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
252	251	fveq2d 6663	. . . . 5 ⊢ (𝜑 → ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
253	100, 107, 252	3eqtrd 2798	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
254	77, 253	oveq12d 7169	. . 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 8779	. . . . 5 ⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin)
257	71	ralrimiva 3114	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
258	12, 18, 256, 257	gsummptcl 19156	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅))
259	12, 13, 101, 84	grprinv 18221	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
260	94, 258, 259	syl2anc 588	. . 3 ⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
261	254, 260	eqtrd 2794	. 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 2798	1 ⊢ (𝜑 → (𝐷‘𝑋) = 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  Vcvv 3410   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4226  {cpr 4525   class class class wbr 5033   ↦ cmpt 5113   I cid 5430   × cxp 5523  dom cdm 5525  ran crn 5526   ↾ cres 5527   ∘ ccom 5529   Fn wfn 6331  ⟶wf 6332  –1-1-onto→wf1o 6335  ‘cfv 6336  (class class class)co 7151  2_oc2o 8107   ↑_m cmap 8417   ≈ cen 8525  Fincfn 8528  1c1 10577   · cmul 10581  -cneg 10910  Basecbs 16542   ↾_s cress 16543  +_gcplusg 16624  ._rcmulr 16625  0_gc0g 16772   Σ_g cgsu 16773   MndHom cmhm 18021  Grpcgrp 18170  inv_gcminusg 18171   GrpHom cghm 18423  SymGrpcsymg 18563  pmTrspcpmtr 18637  pmSgncpsgn 18685  pmEvencevpm 18686  CMndccmn 18974  Abelcabl 18975  mulGrpcmgp 19308  1_rcur 19320  Ringcrg 19366  CRingccrg 19367  ℂ_fldccnfld 20167  ℤRHomczrh 20270   Mat cmat 21108   maDet cmdat 21285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653  ax-addf 10655  ax-mulf 10656

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-xor 1504  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-ot 4532  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-tpos 7903  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-2o 8114  df-er 8300  df-map 8419  df-pm 8420  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8868  df-sup 8940  df-oi 9008  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-div 11337  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-xnn0 12008  df-z 12022  df-dec 12139  df-uz 12284  df-rp 12432  df-fz 12941  df-fzo 13084  df-seq 13420  df-exp 13481  df-hash 13742  df-word 13915  df-lsw 13963  df-concat 13971  df-s1 13998  df-substr 14051  df-pfx 14081  df-splice 14160  df-reverse 14169  df-s2 14258  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-ress 16550  df-plusg 16637  df-mulr 16638  df-starv 16639  df-sca 16640  df-vsca 16641  df-ip 16642  df-tset 16643  df-ple 16644  df-ds 16646  df-unif 16647  df-hom 16648  df-cco 16649  df-0g 16774  df-gsum 16775  df-prds 16780  df-pws 16782  df-mre 16916  df-mrc 16917  df-acs 16919  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-mhm 18023  df-submnd 18024  df-efmnd 18101  df-grp 18173  df-minusg 18174  df-mulg 18293  df-subg 18344  df-ghm 18424  df-gim 18467  df-cntz 18515  df-oppg 18542  df-symg 18564  df-pmtr 18638  df-psgn 18687  df-evpm 18688  df-cmn 18976  df-abl 18977  df-mgp 19309  df-ur 19321  df-ring 19368  df-cring 19369  df-oppr 19445  df-dvdsr 19463  df-unit 19464  df-invr 19494  df-dvr 19505  df-rnghom 19539  df-drng 19573  df-subrg 19602  df-sra 20013  df-rgmod 20014  df-cnfld 20168  df-zring 20240  df-zrh 20274  df-dsmm 20498  df-frlm 20513  df-mat 21109  df-mdet 21286

This theorem is referenced by:  mdetralt2  21310  mdetuni0  21322  mdetmul  21324