Theorem mdetralt 21220

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 21199	. . 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 19311	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
16	14, 15	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
17		ringcmn 19334	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ CMnd)
19	3, 4	matrcl 21024	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
21	20	simpld 497	. . . 4 ⊢ (𝜑 → 𝑁 ∈ Fin)
22		eqid 2824	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
23	22, 5	symgbasfi 18510	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
24	21, 23	syl 17	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
25	16	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
26		zrhpsgnmhm 20731	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
27	16, 21, 26	syl2anc 586	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
28	9, 12	mgpbas 19248	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
29	5, 28	mhmf 17964	. . . . . 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 6854	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
32	9	crngmgp 19308	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
33	14, 32	syl 17	. . . . . 6 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
34	33	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
35	21	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
36	3, 12, 4	matbas2i 21034	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
37	1, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
38		elmapi 8431	. . . . . . . . 9 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
39	37, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
40	39	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
41	22, 5	symgbasf1o 18506	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
42	41	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
43		f1of 6618	. . . . . . . . 9 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
45	44	ffvelrnda 6854	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
46		simpr 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
47	40, 45, 46	fovrnd 7323	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
48	47	ralrimiva 3185	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅))
49	28, 34, 35, 48	gsummptcl 19090	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
50	12, 8	ringcl 19314	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
51	25, 31, 49, 50	syl3anc 1367	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
52		disjdif 4424	. . . 4 ⊢ ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅
53	52	a1i 11	. . 3 ⊢ (𝜑 → ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅)
54	22, 5	evpmss 20733	. . . . . 6 ⊢ (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
55		undif 4433	. . . . . 6 ⊢ ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)))
56	54, 55	mpbi 232	. . . . 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 19054	. 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 5908	. . . . . . 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 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring)
64	21	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin)
65		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁))
66		eqid 2824	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
67	6, 7, 66	zrhpsgnevpm 20738	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
68	63, 64, 65, 67	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅))
69	68	oveq1d 7174	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
70	54	sseli 3966	. . . . . . . . . 10 ⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
71	70, 49	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
72	12, 8, 66	ringlidm 19324	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
73	63, 71, 72	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
74	69, 73	eqtrd 2859	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
75	74	mpteq2dva 5164	. . . . . 6 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
76	62, 75	syl5eq 2871	. . . . 5 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
77	76	oveq2d 7175	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
78		difss 4111	. . . . . . . 8 ⊢ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))
79		resmpt 5908	. . . . . . . 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 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring)
82	21	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin)
83		simpr 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
84		eqid 2824	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
85	6, 7, 66, 5, 84	zrhpsgnodpm 20739	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
86	81, 82, 83, 85	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅)))
87	86	oveq1d 7174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
88		eldifi 4106	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
89	88, 49	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
90	12, 8, 66, 84, 81, 89	ringnegl 19347	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
91	87, 90	eqtrd 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
92	91	mpteq2dva 5164	. . . . . . . 8 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
93		ringgrp 19305	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
94	16, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Grp)
95	12, 84	grpinvf 18153	. . . . . . . . . 10 ⊢ (𝑅 ∈ Grp → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
96	94, 95	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅))
97	96, 89	cofmpt 6897	. . . . . . . 8 ⊢ (𝜑 → ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
98	92, 97	eqtr4d 2862	. . . . . . 7 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
99	80, 98	syl5eq 2871	. . . . . 6 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
100	99	oveq2d 7175	. . . . 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 19333	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
103	16, 102	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Abel)
104		difssd 4112	. . . . . . 7 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)))
105	24, 104	ssfid 8744	. . . . . 6 ⊢ (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
106		eqid 2824	. . . . . 6 ⊢ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
107	12, 101, 84, 103, 105, 89, 106	gsummptfidminv 19070	. . . . 5 ⊢ (𝜑 → (𝑅 Σg ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
108	89	ralrimiva 3185	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
109		mdetralt.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
110		mdetralt.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
111	109, 110	prssd 4758	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁)
112		mdetralt.ij	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
113		pr2nelem 9433	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
114	109, 110, 112, 113	syl3anc 1367	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o)
115		eqid 2824	. . . . . . . . . . . 12 ⊢ (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
116		eqid 2824	. . . . . . . . . . . 12 ⊢ ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
117	115, 116	pmtrrn 18588	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
118	21, 111, 114, 117	syl3anc 1367	. . . . . . . . . 10 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
119	22, 5, 116	pmtrodpm 20744	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
120	21, 118, 119	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
121	22, 5	evpmodpmf1o 20743	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
122	21, 120, 121	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
123	12, 18, 105, 108, 106, 122	gsummptfif1o 19091	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))))
124		eleq1w 2898	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁)))
125	124	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁))))
126		oveq2 7167	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))
127	126	eleq1d 2900	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
128	125, 127	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))))
129	22	symggrp 18531	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
130	21, 129	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp)
131	130	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp)
132	116, 22, 5	symgtrf 18600	. . . . . . . . . . . . . 14 ⊢ ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
133	118	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
134	132, 133	sseldi 3968	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
135	70	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
136		eqid 2824	. . . . . . . . . . . . . 14 ⊢ (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
137	5, 136	grpcl 18114	. . . . . . . . . . . . 13 ⊢ (((SymGrp‘𝑁) ∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
138	131, 134, 135, 137	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
139		eqid 2824	. . . . . . . . . . . . . . . . 17 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})
140	22, 7, 139	psgnghm2 20728	. . . . . . . . . . . . . . . 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 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
143		prex 5336	. . . . . . . . . . . . . . . 16 ⊢ {1, -1} ∈ V
144		eqid 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
145		cnfldmul 20554	. . . . . . . . . . . . . . . . . 18 ⊢ · = (.r‘ℂfld)
146	144, 145	mgpplusg 19246	. . . . . . . . . . . . . . . . 17 ⊢ · = (+g‘(mulGrp‘ℂfld))
147	139, 146	ressplusg 16615	. . . . . . . . . . . . . . . 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 18366	. . . . . . . . . . . . . 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 1367	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
151	22, 116, 7	psgnpmtr 18641	. . . . . . . . . . . . . . . 16 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
152	133, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
153	22, 5, 7	psgnevpm 20736	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
154	21, 153	sylan 582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
155	152, 154	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1))
156		neg1cn 11754	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
157	156	mulid1i 10648	. . . . . . . . . . . . . 14 ⊢ (-1 · 1) = -1
158	155, 157	syl6eq 2875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1)
159	150, 158	eqtrd 2859	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1)
160	22, 5, 7	psgnodpmr 20737	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
161	64, 138, 159, 160	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
162	128, 161	chvarvv 2004	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
163		eqidd 2825	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))
164		eqidd 2825	. . . . . . . . . 10 ⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
165		fveq1 6672	. . . . . . . . . . . . 13 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐))
166	165	oveq1d 7174	. . . . . . . . . . . 12 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))
167	166	mpteq2dv 5165	. . . . . . . . . . 11 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))
168	167	oveq2d 7175	. . . . . . . . . 10 ⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))
169	162, 163, 164, 168	fmptco 6894	. . . . . . . . 9 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))))
170		oveq2 7167	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝))
171	170	fveq1d 6675	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐))
172	171	oveq1d 7174	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))
173	172	mpteq2dv 5165	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))
174	173	oveq2d 7175	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
175	174	cbvmptv 5172	. . . . . . . . . 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 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
178	135	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
179	22, 5, 136	symgov 18515	. . . . . . . . . . . . . . . . 17 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
180	177, 178, 179	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
181	180	fveq1d 6675	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐))
182	70, 44	sylan2 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁)
183		fvco3 6763	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
184	182, 183	sylan 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
185	181, 184	eqtrd 2859	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)))
186	185	oveq1d 7174	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐))
187	115	pmtrprfv 18584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
188	21, 109, 110, 112, 187	syl13anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
189	188	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
190	189	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐))
191		oveq2 7167	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐))
192		oveq2 7167	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐))
193	191, 192	eqeq12d 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐)))
194		mdetralt.eq	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
195	194	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
196		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
197	193, 195, 196	rspcdva 3628	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐))
198	190, 197	eqtr4d 2862	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))
199		fveq2 6673	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼))
200	199	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐))
201		oveq1 7166	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐))
202	200, 201	eqeq12d 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)))
203	198, 202	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
204		prcom 4671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
205	204	fveq2i 6676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼})
206	205	fveq1i 6674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽)
207	112	necomd 3074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
208	115	pmtrprfv 18584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
209	21, 110, 109, 207, 208	syl13anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
210	206, 209	syl5eq 2871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼)
211	210	oveq1d 7174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
212	211	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
213	212, 197	eqtrd 2859	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))
214		fveq2 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽))
215	214	oveq1d 7174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐))
216		oveq1 7166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐))
217	215, 216	eqeq12d 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)))
218	213, 217	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
219	218	a1dd 50	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
220		neanior 3112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
221		elpri 4592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽))
222	221	orcomd 867	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼))
223	222	con3i 157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
224	220, 223	sylbi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
225	224	3adant1 1126	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽})
226	115	pmtrmvd 18587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
227	21, 111, 114, 226	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
228	227	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
229	228	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
230	225, 229	neleqtrrd 2938	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))
231	115	pmtrf 18586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
232	21, 111, 114, 231	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁)
233	232	ffnd 6518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
234	233	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
235	182	ffvelrnda 6854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
236		fnelnfp 6942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
237	234, 235, 236	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
238	237	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐)))
239	238	necon2bbid 3062	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )))
240	230, 239	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐))
241	240	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
242	241	3exp 1115	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))))
243	219, 242	pm2.61dne 3106	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))
244	203, 243	pm2.61dne 3106	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
245	186, 244	eqtrd 2859	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))
246	245	mpteq2dva 5164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))
247	246	oveq2d 7175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))
248	247	mpteq2dva 5164	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
249	169, 176, 248	3eqtrd 2863	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))
250	249	oveq2d 7175	. . . . . . 7 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
251	123, 250	eqtrd 2859	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))
252	251	fveq2d 6677	. . . . 5 ⊢ (𝜑 → ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
253	100, 107, 252	3eqtrd 2863	. . . 4 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))
254	77, 253	oveq12d 7177	. . 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 8744	. . . . 5 ⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin)
257	71	ralrimiva 3185	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
258	12, 18, 256, 257	gsummptcl 19090	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅))
259	12, 13, 101, 84	grprinv 18156	. . . 4 ⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
260	94, 258, 259	syl2anc 586	. . 3 ⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 )
261	254, 260	eqtrd 2859	. 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 2863	1 ⊢ (𝜑 → (𝐷‘𝑋) = 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  Vcvv 3497   ∖ cdif 3936   ∪ cun 3937   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  {cpr 4572   class class class wbr 5069   ↦ cmpt 5149   I cid 5462   × cxp 5556  dom cdm 5558  ran crn 5559   ↾ cres 5560   ∘ ccom 5562   Fn wfn 6353  ⟶wf 6354  –1-1-onto→wf1o 6357  ‘cfv 6358  (class class class)co 7159  2_oc2o 8099   ↑_m cmap 8409   ≈ cen 8509  Fincfn 8512  1c1 10541   · cmul 10545  -cneg 10874  Basecbs 16486   ↾_s cress 16487  +_gcplusg 16568  ._rcmulr 16569  0_gc0g 16716   Σ_g cgsu 16717   MndHom cmhm 17957  Grpcgrp 18106  inv_gcminusg 18107   GrpHom cghm 18358  SymGrpcsymg 18498  pmTrspcpmtr 18572  pmSgncpsgn 18620  pmEvencevpm 18621  CMndccmn 18909  Abelcabl 18910  mulGrpcmgp 19242  1_rcur 19254  Ringcrg 19300  CRingccrg 19301  ℂ_fldccnfld 20548  ℤRHomczrh 20650   Mat cmat 21019   maDet cmdat 21196

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-cnex 10596  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616  ax-pre-mulgt0 10617  ax-addf 10619  ax-mulf 10620

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-xor 1502  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-ot 4579  df-uni 4842  df-int 4880  df-iun 4924  df-iin 4925  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-se 5518  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-of 7412  df-om 7584  df-1st 7692  df-2nd 7693  df-supp 7834  df-tpos 7895  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8465  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516  df-fsupp 8837  df-sup 8909  df-oi 8977  df-card 9371  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-sub 10875  df-neg 10876  df-div 11301  df-nn 11642  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-xnn0 11971  df-z 11985  df-dec 12102  df-uz 12247  df-rp 12393  df-fz 12896  df-fzo 13037  df-seq 13373  df-exp 13433  df-hash 13694  df-word 13865  df-lsw 13918  df-concat 13926  df-s1 13953  df-substr 14006  df-pfx 14036  df-splice 14115  df-reverse 14124  df-s2 14213  df-struct 16488  df-ndx 16489  df-slot 16490  df-base 16492  df-sets 16493  df-ress 16494  df-plusg 16581  df-mulr 16582  df-starv 16583  df-sca 16584  df-vsca 16585  df-ip 16586  df-tset 16587  df-ple 16588  df-ds 16590  df-unif 16591  df-hom 16592  df-cco 16593  df-0g 16718  df-gsum 16719  df-prds 16724  df-pws 16726  df-mre 16860  df-mrc 16861  df-acs 16863  df-mgm 17855  df-sgrp 17904  df-mnd 17915  df-mhm 17959  df-submnd 17960  df-efmnd 18037  df-grp 18109  df-minusg 18110  df-mulg 18228  df-subg 18279  df-ghm 18359  df-gim 18402  df-cntz 18450  df-oppg 18477  df-symg 18499  df-pmtr 18573  df-psgn 18622  df-evpm 18623  df-cmn 18911  df-abl 18912  df-mgp 19243  df-ur 19255  df-ring 19302  df-cring 19303  df-oppr 19376  df-dvdsr 19394  df-unit 19395  df-invr 19425  df-dvr 19436  df-rnghom 19470  df-drng 19507  df-subrg 19536  df-sra 19947  df-rgmod 19948  df-cnfld 20549  df-zring 20621  df-zrh 20654  df-dsmm 20879  df-frlm 20894  df-mat 21020  df-mdet 21197

This theorem is referenced by:  mdetralt2  21221  mdetuni0  21233  mdetmul  21235