Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetralt Structured version   Visualization version   GIF version

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.
StepHypRef 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‘𝑅)
102, 3, 4, 5, 6, 7, 8, 9mdetleib 21288 . . 3 (𝑋𝐵 → (𝐷𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))))
111, 10syl 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)
1614, 15syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
17 ringcmn 19403 . . . 4 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
1816, 17syl 17 . . 3 (𝜑𝑅 ∈ CMnd)
193, 4matrcl 21113 . . . . . 6 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
201, 19syl 17 . . . . 5 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
2120simpld 499 . . . 4 (𝜑𝑁 ∈ Fin)
22 eqid 2759 . . . . 5 (SymGrp‘𝑁) = (SymGrp‘𝑁)
2322, 5symgbasfi 18575 . . . 4 (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
2421, 23syl 17 . . 3 (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
2516adantr 485 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
26 zrhpsgnmhm 20350 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2716, 21, 26syl2anc 588 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
289, 12mgpbas 19314 . . . . . . 7 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
295, 28mhmf 18028 . . . . . 6 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
3027, 29syl 17 . . . . 5 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
3130ffvelrnda 6843 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
329crngmgp 19374 . . . . . . 7 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
3314, 32syl 17 . . . . . 6 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
3433adantr 485 . . . . 5 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
3521adantr 485 . . . . 5 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
363, 12, 4matbas2i 21123 . . . . . . . . . 10 (𝑋𝐵𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
371, 36syl 17 . . . . . . . . 9 (𝜑𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
38 elmapi 8439 . . . . . . . . 9 (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
3937, 38syl 17 . . . . . . . 8 (𝜑𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
4039ad2antrr 726 . . . . . . 7 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
4122, 5symgbasf1o 18571 . . . . . . . . . 10 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁1-1-onto𝑁)
4241adantl 486 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁1-1-onto𝑁)
43 f1of 6603 . . . . . . . . 9 (𝑝:𝑁1-1-onto𝑁𝑝:𝑁𝑁)
4442, 43syl 17 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁𝑁)
4544ffvelrnda 6843 . . . . . . 7 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐𝑁) → (𝑝𝑐) ∈ 𝑁)
46 simpr 489 . . . . . . 7 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐𝑁) → 𝑐𝑁)
4740, 45, 46fovrnd 7317 . . . . . 6 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐𝑁) → ((𝑝𝑐)𝑋𝑐) ∈ (Base‘𝑅))
4847ralrimiva 3114 . . . . 5 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐𝑁 ((𝑝𝑐)𝑋𝑐) ∈ (Base‘𝑅))
4928, 34, 35, 48gsummptcl 19156 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
5012, 8ringcl 19383 . . . 4 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
5125, 31, 49, 50syl3anc 1369 . . 3 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) ∈ (Base‘𝑅))
52 disjdif 4369 . . . 4 ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅
5352a1i 11 . . 3 (𝜑 → ((pmEven‘𝑁) ∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅)
5422, 5evpmss 20352 . . . . . 6 (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
55 undif 4379 . . . . . 6 ((pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)))
5654, 55mpbi 233 . . . . 5 ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁))
5756eqcomi 2768 . . . 4 (Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
5857a1i 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 (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
6012, 13, 18, 24, 51, 53, 58, 59gsummptfidmsplitres 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 (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
6254, 61ax-mp 5 . . . . . 6 ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
6316adantr 485 . . . . . . . . . 10 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring)
6421adantr 485 . . . . . . . . . 10 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin)
65 simpr 489 . . . . . . . . . 10 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁))
66 eqid 2759 . . . . . . . . . . 11 (1r𝑅) = (1r𝑅)
676, 7, 66zrhpsgnevpm 20357 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r𝑅))
6863, 64, 65, 67syl3anc 1369 . . . . . . . . 9 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r𝑅))
6968oveq1d 7166 . . . . . . . 8 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((1r𝑅)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
7054sseli 3889 . . . . . . . . . 10 (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
7170, 49sylan2 596 . . . . . . . . 9 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
7212, 8, 66ringlidm 19393 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r𝑅)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))
7363, 71, 72syl2anc 588 . . . . . . . 8 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((1r𝑅)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))
7469, 73eqtrd 2794 . . . . . . 7 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))
7574mpteq2dva 5128 . . . . . 6 (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
7662, 75syl5eq 2806 . . . . 5 (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
7776oveq2d 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 (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
8078, 79ax-mp 5 . . . . . . 7 ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
8116adantr 485 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring)
8221adantr 485 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin)
83 simpr 489 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
84 eqid 2759 . . . . . . . . . . . . 13 (invg𝑅) = (invg𝑅)
856, 7, 66, 5, 84zrhpsgnodpm 20358 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg𝑅)‘(1r𝑅)))
8681, 82, 83, 85syl3anc 1369 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg𝑅)‘(1r𝑅)))
8786oveq1d 7166 . . . . . . . . . 10 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = (((invg𝑅)‘(1r𝑅))(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
88 eldifi 4033 . . . . . . . . . . . 12 (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
8988, 49sylan2 596 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
9012, 8, 66, 84, 81, 89ringnegl 19416 . . . . . . . . . 10 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((invg𝑅)‘(1r𝑅))(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((invg𝑅)‘((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
9187, 90eqtrd 2794 . . . . . . . . 9 ((𝜑𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = ((invg𝑅)‘((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
9291mpteq2dva 5128 . . . . . . . 8 (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg𝑅)‘((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
93 ringgrp 19371 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
9416, 93syl 17 . . . . . . . . . 10 (𝜑𝑅 ∈ Grp)
9512, 84grpinvf 18218 . . . . . . . . . 10 (𝑅 ∈ Grp → (invg𝑅):(Base‘𝑅)⟶(Base‘𝑅))
9694, 95syl 17 . . . . . . . . 9 (𝜑 → (invg𝑅):(Base‘𝑅)⟶(Base‘𝑅))
9796, 89cofmpt 6886 . . . . . . . 8 (𝜑 → ((invg𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((invg𝑅)‘((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
9892, 97eqtr4d 2797 . . . . . . 7 (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = ((invg𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
9980, 98syl5eq 2806 . . . . . 6 (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
10099oveq2d 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)
10316, 102syl 17 . . . . . 6 (𝜑𝑅 ∈ Abel)
104 difssd 4039 . . . . . . 7 (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)))
10524, 104ssfid 8779 . . . . . 6 (𝜑 → ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin)
106 eqid 2759 . . . . . 6 (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))
10712, 101, 84, 103, 105, 89, 106gsummptfidminv 19136 . . . . 5 (𝜑 → (𝑅 Σg ((invg𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))) = ((invg𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))))
10889ralrimiva 3114 . . . . . . . 8 (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
109 mdetralt.i . . . . . . . . . . . 12 (𝜑𝐼𝑁)
110 mdetralt.j . . . . . . . . . . . 12 (𝜑𝐽𝑁)
111109, 110prssd 4713 . . . . . . . . . . 11 (𝜑 → {𝐼, 𝐽} ⊆ 𝑁)
112 mdetralt.ij . . . . . . . . . . . 12 (𝜑𝐼𝐽)
113 pr2nelem 9465 . . . . . . . . . . . 12 ((𝐼𝑁𝐽𝑁𝐼𝐽) → {𝐼, 𝐽} ≈ 2o)
114109, 110, 112, 113syl3anc 1369 . . . . . . . . . . 11 (𝜑 → {𝐼, 𝐽} ≈ 2o)
115 eqid 2759 . . . . . . . . . . . 12 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
116 eqid 2759 . . . . . . . . . . . 12 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
117115, 116pmtrrn 18653 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
11821, 111, 114, 117syl3anc 1369 . . . . . . . . . 10 (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
11922, 5, 116pmtrodpm 20363 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
12021, 118, 119syl2anc 588 . . . . . . . . 9 (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
12122, 5evpmodpmf1o 20362 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
12221, 120, 121syl2anc 588 . . . . . . . 8 (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
12312, 18, 105, 108, 106, 122gsummptfif1o 19157 . . . . . . 7 (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))))
124 eleq1w 2835 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁)))
125124anbi2d 632 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝜑𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑𝑞 ∈ (pmEven‘𝑁))))
126 oveq2 7159 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))
127126eleq1d 2837 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))
128125, 127imbi12d 349 . . . . . . . . . . 11 (𝑝 = 𝑞 → (((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))))
12922symggrp 18596 . . . . . . . . . . . . . . 15 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
13021, 129syl 17 . . . . . . . . . . . . . 14 (𝜑 → (SymGrp‘𝑁) ∈ Grp)
131130adantr 485 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp)
132116, 22, 5symgtrf 18665 . . . . . . . . . . . . . 14 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
133118adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁))
134132, 133sseldi 3891 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
13570adantl 486 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
136 eqid 2759 . . . . . . . . . . . . . 14 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
1375, 136grpcl 18178 . . . . . . . . . . . . 13 (((SymGrp‘𝑁) ∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
138131, 134, 135, 137syl3anc 1369 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)))
139 eqid 2759 . . . . . . . . . . . . . . . . 17 ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})
14022, 7, 139psgnghm2 20347 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Fin → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
14121, 140syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})))
142141adantr 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)
146144, 145mgpplusg 19312 . . . . . . . . . . . . . . . . 17 · = (+g‘(mulGrp‘ℂfld))
147139, 146ressplusg 16671 . . . . . . . . . . . . . . . 16 ({1, -1} ∈ V → · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1})))
148143, 147ax-mp 5 . . . . . . . . . . . . . . 15 · = (+g‘((mulGrp‘ℂfld) ↾s {1, -1}))
1495, 136, 148ghmlin 18431 . . . . . . . . . . . . . 14 (((pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})) ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
150142, 134, 135, 149syl3anc 1369 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)))
15122, 116, 7psgnpmtr 18706 . . . . . . . . . . . . . . . 16 (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
152133, 151syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1)
15322, 5, 7psgnevpm 20355 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
15421, 153sylan 584 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1)
155152, 154oveq12d 7169 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1))
156 neg1cn 11789 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
157156mulid1i 10684 . . . . . . . . . . . . . 14 (-1 · 1) = -1
158155, 157eqtrdi 2810 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1)
159150, 158eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1)
16022, 5, 7psgnodpmr 20356 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
16164, 138, 159, 160syl3anc 1369 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
162128, 161chvarvv 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‘𝑁))𝑞)‘𝑐))
166165oveq1d 7166 . . . . . . . . . . . 12 (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))
167166mpteq2dv 5129 . . . . . . . . . . 11 (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)) = (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))
168167oveq2d 7167 . . . . . . . . . 10 (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))
169162, 163, 164, 168fmptco 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‘𝑁))𝑝))
171170fveq1d 6661 . . . . . . . . . . . . . 14 (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐))
172171oveq1d 7166 . . . . . . . . . . . . 13 (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))
173172mpteq2dv 5129 . . . . . . . . . . . 12 (𝑞 = 𝑝 → (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))
174173oveq2d 7167 . . . . . . . . . . 11 (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
175174cbvmptv 5136 . . . . . . . . . 10 (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))
176175a1i 11 . . . . . . . . 9 (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))))
177134adantr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)))
178135adantr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁)))
17922, 5, 136symgov 18580 . . . . . . . . . . . . . . . . 17 ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
180177, 178, 179syl2anc 588 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝))
181180fveq1d 6661 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐))
18270, 44sylan2 596 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁𝑁)
183 fvco3 6752 . . . . . . . . . . . . . . . 16 ((𝑝:𝑁𝑁𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)))
184182, 183sylan 584 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)))
185181, 184eqtrd 2794 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)))
186185oveq1d 7166 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐))
187115pmtrprfv 18649 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ Fin ∧ (𝐼𝑁𝐽𝑁𝐼𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
18821, 109, 110, 112, 187syl13anc 1370 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
189188ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽)
190189oveq1d 7166 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐))
191 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐))
192 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐))
193191, 192eqeq12d 2775 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐)))
194 mdetralt.eq . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑎𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
195194ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ∀𝑎𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))
196 simpr 489 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → 𝑐𝑁)
197193, 195, 196rspcdva 3544 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐))
198190, 197eqtr4d 2797 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))
199 fveq2 6659 . . . . . . . . . . . . . . . . 17 ((𝑝𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼))
200199oveq1d 7166 . . . . . . . . . . . . . . . 16 ((𝑝𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐))
201 oveq1 7158 . . . . . . . . . . . . . . . 16 ((𝑝𝑐) = 𝐼 → ((𝑝𝑐)𝑋𝑐) = (𝐼𝑋𝑐))
202200, 201eqeq12d 2775 . . . . . . . . . . . . . . 15 ((𝑝𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)))
203198, 202syl5ibrcom 250 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐)))
204 prcom 4626 . . . . . . . . . . . . . . . . . . . . . . 23 {𝐼, 𝐽} = {𝐽, 𝐼}
205204fveq2i 6662 . . . . . . . . . . . . . . . . . . . . . 22 ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼})
206205fveq1i 6660 . . . . . . . . . . . . . . . . . . . . 21 (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽)
207112necomd 3007 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽𝐼)
208115pmtrprfv 18649 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ Fin ∧ (𝐽𝑁𝐼𝑁𝐽𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
20921, 110, 109, 207, 208syl13anc 1370 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼)
210206, 209syl5eq 2806 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼)
211210oveq1d 7166 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
212211ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐))
213212, 197eqtrd 2794 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))
214 fveq2 6659 . . . . . . . . . . . . . . . . . . 19 ((𝑝𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽))
215214oveq1d 7166 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐))
216 oveq1 7158 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑐) = 𝐽 → ((𝑝𝑐)𝑋𝑐) = (𝐽𝑋𝑐))
217215, 216eqeq12d 2775 . . . . . . . . . . . . . . . . 17 ((𝑝𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)))
218213, 217syl5ibrcom 250 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐)))
219218a1dd 50 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) = 𝐽 → ((𝑝𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐))))
220 neanior 3044 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) ↔ ¬ ((𝑝𝑐) = 𝐽 ∨ (𝑝𝑐) = 𝐼))
221 elpri 4545 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝𝑐) ∈ {𝐼, 𝐽} → ((𝑝𝑐) = 𝐼 ∨ (𝑝𝑐) = 𝐽))
222221orcomd 869 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝𝑐) ∈ {𝐼, 𝐽} → ((𝑝𝑐) = 𝐽 ∨ (𝑝𝑐) = 𝐼))
223222con3i 157 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑝𝑐) = 𝐽 ∨ (𝑝𝑐) = 𝐼) → ¬ (𝑝𝑐) ∈ {𝐼, 𝐽})
224220, 223sylbi 220 . . . . . . . . . . . . . . . . . . . 20 (((𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ¬ (𝑝𝑐) ∈ {𝐼, 𝐽})
2252243adant1 1128 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ¬ (𝑝𝑐) ∈ {𝐼, 𝐽})
226115pmtrmvd 18652 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
22721, 111, 114, 226syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
228227ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
2292283ad2ant1 1131 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽})
230225, 229neleqtrrd 2875 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ¬ (𝑝𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))
231115pmtrf 18651 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁𝑁)
23221, 111, 114, 231syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁𝑁)
233232ffnd 6500 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
234233ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁)
235182ffvelrnda 6843 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (𝑝𝑐) ∈ 𝑁)
236 fnelnfp 6931 . . . . . . . . . . . . . . . . . . . . 21 ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝𝑐) ∈ 𝑁) → ((𝑝𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) ≠ (𝑝𝑐)))
237234, 235, 236syl2anc 588 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) ≠ (𝑝𝑐)))
2382373ad2ant1 1131 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ((𝑝𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) ≠ (𝑝𝑐)))
239238necon2bbid 2995 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) = (𝑝𝑐) ↔ ¬ (𝑝𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )))
240230, 239mpbird 260 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐)) = (𝑝𝑐))
241240oveq1d 7166 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) ∧ (𝑝𝑐) ≠ 𝐽 ∧ (𝑝𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐))
2422413exp 1117 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) ≠ 𝐽 → ((𝑝𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐))))
243219, 242pm2.61dne 3038 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((𝑝𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐)))
244203, 243pm2.61dne 3038 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝𝑐))𝑋𝑐) = ((𝑝𝑐)𝑋𝑐))
245186, 244eqtrd 2794 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝𝑐)𝑋𝑐))
246245mpteq2dva 5128 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))
247246oveq2d 7167 . . . . . . . . . 10 ((𝜑𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))
248247mpteq2dva 5128 . . . . . . . . 9 (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
249169, 176, 2483eqtrd 2798 . . . . . . . 8 (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))
250249oveq2d 7167 . . . . . . 7 (𝜑 → (𝑅 Σg ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
251123, 250eqtrd 2794 . . . . . 6 (𝜑 → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))
252251fveq2d 6663 . . . . 5 (𝜑 → ((invg𝑅)‘(𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))) = ((invg𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))))
253100, 107, 2523eqtrd 2798 . . . 4 (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))))
25477, 253oveq12d 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 (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))))
25554a1i 11 . . . . . 6 (𝜑 → (pmEven‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
25624, 255ssfid 8779 . . . . 5 (𝜑 → (pmEven‘𝑁) ∈ Fin)
25771ralrimiva 3114 . . . . 5 (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))) ∈ (Base‘𝑅))
25812, 18, 256, 257gsummptcl 19156 . . . 4 (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ∈ (Base‘𝑅))
25912, 13, 101, 84grprinv 18221 . . . 4 ((𝑅 ∈ Grp ∧ (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))(+g𝑅)((invg𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))) = 0 )
26094, 258, 259syl2anc 588 . . 3 (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐)))))(+g𝑅)((invg𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))))) = 0 )
261254, 260eqtrd 2794 . 2 (𝜑 → ((𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g𝑅)(𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑐𝑁 ↦ ((𝑝𝑐)𝑋𝑐))))) ↾ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) = 0 )
26211, 60, 2613eqtrd 2798 1 (𝜑 → (𝐷𝑋) = 0 )
 Colors of variables: wff setvar class 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  2oc2o 8107   ↑m cmap 8417   ≈ cen 8525  Fincfn 8528  1c1 10577   · cmul 10581  -cneg 10910  Basecbs 16542   ↾s cress 16543  +gcplusg 16624  .rcmulr 16625  0gc0g 16772   Σg cgsu 16773   MndHom cmhm 18021  Grpcgrp 18170  invgcminusg 18171   GrpHom cghm 18423  SymGrpcsymg 18563  pmTrspcpmtr 18637  pmSgncpsgn 18685  pmEvencevpm 18686  CMndccmn 18974  Abelcabl 18975  mulGrpcmgp 19308  1rcur 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
 Copyright terms: Public domain W3C validator