| 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 2737 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
| 6 | | eqid 2737 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
| 7 | | eqid 2737 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
| 8 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 9 | | eqid 2737 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | mdetleib 22593 |
. . 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 2737 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 13 | | eqid 2737 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 14 | | mdetralt.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 15 | | crngring 20242 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 17 | | ringcmn 20279 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 19 | 3, 4 | matrcl 22416 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 20 | 1, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 21 | 20 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 22 | | eqid 2737 |
. . . . 5
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
| 23 | 22, 5 | symgbasfi 19396 |
. . . 4
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 24 | 21, 23 | syl 17 |
. . 3
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 25 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
| 26 | | zrhpsgnmhm 21602 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
| 27 | 16, 21, 26 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
| 28 | 9, 12 | mgpbas 20142 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 29 | 5, 28 | mhmf 18802 |
. . . . . 6
⊢
(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅)) |
| 30 | 27, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅)) |
| 31 | 30 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅)) |
| 32 | 9 | crngmgp 20238 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
| 33 | 14, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd) |
| 35 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin) |
| 36 | 3, 12, 4 | matbas2i 22428 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 37 | 1, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 38 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 40 | 39 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 41 | 22, 5 | symgbasf1o 19392 |
. . . . . . . . . 10
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁) |
| 42 | 41 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁) |
| 43 | | f1of 6848 |
. . . . . . . . 9
⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁) |
| 44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁) |
| 45 | 44 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁) |
| 46 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
| 47 | 40, 45, 46 | fovcdmd 7605 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅)) |
| 48 | 47 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅)) |
| 49 | 28, 34, 35, 48 | gsummptcl 19985 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
| 50 | 12, 8 | ringcl 20247 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅)) |
| 51 | 25, 31, 49, 50 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅)) |
| 52 | | disjdif 4472 |
. . . 4
⊢
((pmEven‘𝑁)
∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅ |
| 53 | 52 | a1i 11 |
. . 3
⊢ (𝜑 → ((pmEven‘𝑁) ∩
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅) |
| 54 | 22, 5 | evpmss 21604 |
. . . . . 6
⊢
(pmEven‘𝑁)
⊆ (Base‘(SymGrp‘𝑁)) |
| 55 | | undif 4482 |
. . . . . 6
⊢
((pmEven‘𝑁)
⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) =
(Base‘(SymGrp‘𝑁))) |
| 56 | 54, 55 | mpbi 230 |
. . . . 5
⊢
((pmEven‘𝑁)
∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (Base‘(SymGrp‘𝑁)) |
| 57 | 56 | eqcomi 2746 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 58 | 57 | a1i 11 |
. . 3
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) = ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) |
| 59 | | eqid 2737 |
. . 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 19949 |
. 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 6055 |
. . . . . . 7
⊢
((pmEven‘𝑁)
⊆ (Base‘(SymGrp‘𝑁)) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 62 | 54, 61 | ax-mp 5 |
. . . . . 6
⊢ ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 63 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring) |
| 64 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin) |
| 65 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁)) |
| 66 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 67 | 6, 7, 66 | zrhpsgnevpm 21609 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅)) |
| 68 | 63, 64, 65, 67 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅)) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 70 | 54 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
| 71 | 70, 49 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
| 72 | 12, 8, 66 | ringlidm 20266 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
| 73 | 63, 71, 72 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
| 74 | 69, 73 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
| 75 | 74 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 76 | 62, 75 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 77 | 76 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 78 | | difss 4136 |
. . . . . . . 8
⊢
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)) |
| 79 | | resmpt 6055 |
. . . . . . . 8
⊢
(((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 80 | 78, 79 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 81 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring) |
| 82 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin) |
| 83 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 84 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 85 | 6, 7, 66, 5, 84 | zrhpsgnodpm 21610 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅))) |
| 86 | 81, 82, 83, 85 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅))) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 88 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
| 89 | 88, 49 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
| 90 | 12, 8, 66, 84, 81, 89 | ringnegl 20299 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
(((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 91 | 87, 90 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 92 | 91 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 93 | | ringgrp 20235 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 94 | 16, 93 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 95 | 12, 84 | grpinvf 19004 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
| 96 | 94, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
| 97 | 96, 89 | cofmpt 7152 |
. . . . . . . 8
⊢ (𝜑 →
((invg‘𝑅)
∘ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 98 | 92, 97 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 99 | 80, 98 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 100 | 99 | oveq2d 7447 |
. . . . 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 20278 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel) |
| 103 | 16, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Abel) |
| 104 | | difssd 4137 |
. . . . . . 7
⊢ (𝜑 →
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))) |
| 105 | 24, 104 | ssfid 9301 |
. . . . . 6
⊢ (𝜑 →
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin) |
| 106 | | eqid 2737 |
. . . . . 6
⊢ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
| 107 | 12, 101, 84, 103, 105, 89, 106 | gsummptfidminv 19965 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg
((invg‘𝑅)
∘ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
| 108 | 89 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
| 109 | | mdetralt.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ 𝑁) |
| 110 | | mdetralt.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ 𝑁) |
| 111 | 109, 110 | prssd 4822 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁) |
| 112 | | mdetralt.ij |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ≠ 𝐽) |
| 113 | | enpr2 10042 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o) |
| 114 | 109, 110,
112, 113 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o) |
| 115 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(pmTrsp‘𝑁) =
(pmTrsp‘𝑁) |
| 116 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ran
(pmTrsp‘𝑁) = ran
(pmTrsp‘𝑁) |
| 117 | 115, 116 | pmtrrn 19475 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) →
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
| 118 | 21, 111, 114, 117 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
| 119 | 22, 5, 116 | pmtrodpm 21615 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 120 | 21, 118, 119 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 121 | 22, 5 | evpmodpmf1o 21614 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 122 | 21, 120, 121 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 123 | 12, 18, 105, 108, 106, 122 | gsummptfif1o 19986 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))))) |
| 124 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁))) |
| 125 | 124 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)))) |
| 126 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) |
| 127 | 126 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) |
| 128 | 125, 127 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) |
| 129 | 22 | symggrp 19418 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ Fin →
(SymGrp‘𝑁) ∈
Grp) |
| 130 | 21, 129 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp) |
| 131 | 130 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp) |
| 132 | 116, 22, 5 | symgtrf 19487 |
. . . . . . . . . . . . . 14
⊢ ran
(pmTrsp‘𝑁) ⊆
(Base‘(SymGrp‘𝑁)) |
| 133 | 118 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
| 134 | 132, 133 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁))) |
| 135 | 70 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
| 136 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
| 137 | 5, 136 | grpcl 18959 |
. . . . . . . . . . . . 13
⊢
(((SymGrp‘𝑁)
∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁))) |
| 138 | 131, 134,
135, 137 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁))) |
| 139 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
| 140 | 22, 7, 139 | psgnghm2 21599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ Fin →
(pmSgn‘𝑁) ∈
((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
| 141 | 21, 140 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
| 142 | 141 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
| 143 | | prex 5437 |
. . . . . . . . . . . . . . . 16
⊢ {1, -1}
∈ V |
| 144 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 145 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
| 146 | 144, 145 | mgpplusg 20141 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 147 | 139, 146 | ressplusg 17334 |
. . . . . . . . . . . . . . . 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 19239 |
. . . . . . . . . . . . . 14
⊢
(((pmSgn‘𝑁)
∈ ((SymGrp‘𝑁)
GrpHom ((mulGrp‘ℂfld) ↾s {1, -1}))
∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝))) |
| 150 | 142, 134,
135, 149 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝))) |
| 151 | 22, 116, 7 | psgnpmtr 19528 |
. . . . . . . . . . . . . . . 16
⊢
(((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1) |
| 152 | 133, 151 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1) |
| 153 | 22, 5, 7 | psgnevpm 21607 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1) |
| 154 | 21, 153 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1) |
| 155 | 152, 154 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1)) |
| 156 | | neg1cn 12380 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
| 157 | 156 | mulridi 11265 |
. . . . . . . . . . . . . 14
⊢ (-1
· 1) = -1 |
| 158 | 155, 157 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1) |
| 159 | 150, 158 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) |
| 160 | 22, 5, 7 | psgnodpmr 21608 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧
(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 161 | 64, 138, 159, 160 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 162 | 128, 161 | chvarvv 1998 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
| 163 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) |
| 164 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 165 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)) |
| 166 | 165 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) |
| 167 | 166 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) |
| 168 | 167 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) |
| 169 | 162, 163,
164, 168 | fmptco 7149 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))) |
| 170 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) |
| 171 | 170 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)) |
| 172 | 171 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) |
| 173 | 172 | mpteq2dv 5244 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) |
| 174 | 173 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) |
| 175 | 174 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) |
| 176 | 175 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))) |
| 177 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁))) |
| 178 | 135 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
| 179 | 22, 5, 136 | symgov 19401 |
. . . . . . . . . . . . . . . . 17
⊢
((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)) |
| 180 | 177, 178,
179 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)) |
| 181 | 180 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐)) |
| 182 | 70, 44 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁) |
| 183 | | fvco3 7008 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
| 184 | 182, 183 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
| 185 | 181, 184 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
| 186 | 185 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐)) |
| 187 | 115 | pmtrprfv 19471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
| 188 | 21, 109, 110, 112, 187 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
| 189 | 188 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
| 190 | 189 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐)) |
| 191 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐)) |
| 192 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐)) |
| 193 | 191, 192 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐))) |
| 194 | | mdetralt.eq |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎)) |
| 195 | 194 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎)) |
| 196 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
| 197 | 193, 195,
196 | rspcdva 3623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐)) |
| 198 | 190, 197 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)) |
| 199 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)) |
| 200 | 199 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐)) |
| 201 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐)) |
| 202 | 200, 201 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))) |
| 203 | 198, 202 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
| 204 | | prcom 4732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝐼, 𝐽} = {𝐽, 𝐼} |
| 205 | 204 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼}) |
| 206 | 205 | fveq1i 6907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) |
| 207 | 112 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
| 208 | 115 | pmtrprfv 19471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼) |
| 209 | 21, 110, 109, 207, 208 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼) |
| 210 | 206, 209 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼) |
| 211 | 210 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐)) |
| 212 | 211 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐)) |
| 213 | 212, 197 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)) |
| 214 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)) |
| 215 | 214 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐)) |
| 216 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐)) |
| 217 | 215, 216 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))) |
| 218 | 213, 217 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
| 219 | 218 | a1dd 50 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))) |
| 220 | | neanior 3035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼)) |
| 221 | | elpri 4649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽)) |
| 222 | 221 | orcomd 872 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼)) |
| 223 | 222 | con3i 154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
| 224 | 220, 223 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
| 225 | 224 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
| 226 | 115 | pmtrmvd 19474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom
(((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 227 | 21, 111, 114, 226 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 228 | 227 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 229 | 228 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
| 230 | 225, 229 | neleqtrrd 2864 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )) |
| 231 | 115 | pmtrf 19473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) →
((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁) |
| 232 | 21, 111, 114, 231 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁) |
| 233 | 232 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁) |
| 234 | 233 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁) |
| 235 | 182 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁) |
| 236 | | fnelnfp 7197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
| 237 | 234, 235,
236 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
| 238 | 237 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
| 239 | 238 | necon2bbid 2984 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))) |
| 240 | 230, 239 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐)) |
| 241 | 240 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
| 242 | 241 | 3exp 1120 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))) |
| 243 | 219, 242 | pm2.61dne 3028 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
| 244 | 203, 243 | pm2.61dne 3028 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
| 245 | 186, 244 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
| 246 | 245 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) |
| 247 | 246 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
| 248 | 247 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 249 | 169, 176,
248 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
| 250 | 249 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 251 | 123, 250 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
| 252 | 251 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 →
((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
| 253 | 100, 107,
252 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
| 254 | 77, 253 | oveq12d 7449 |
. . 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 9301 |
. . . . 5
⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin) |
| 257 | 71 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
| 258 | 12, 18, 256, 257 | gsummptcl 19985 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) |
| 259 | 12, 13, 101, 84 | grprinv 19008 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg
(𝑝 ∈
(pmEven‘𝑁) ↦
((mulGrp‘𝑅)
Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 ) |
| 260 | 94, 258, 259 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 ) |
| 261 | 254, 260 | eqtrd 2777 |
. 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 2781 |
1
⊢ (𝜑 → (𝐷‘𝑋) = 0 ) |