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 20760 |
. . 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 18911 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
17 | | ringcmn 18934 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CMnd) |
19 | 3, 4 | matrcl 20584 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
20 | 1, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
21 | 20 | simpld 490 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
22 | | eqid 2824 |
. . . . 5
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
23 | 22, 5 | symgbasfi 18155 |
. . . 4
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
24 | 21, 23 | syl 17 |
. . 3
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
25 | 16 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
26 | | zrhpsgnmhm 20288 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
27 | 16, 21, 26 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
28 | 9, 12 | mgpbas 18848 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
29 | 5, 28 | mhmf 17692 |
. . . . . 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 6607 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅)) |
32 | 9 | crngmgp 18908 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
33 | 14, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
34 | 33 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd) |
35 | 21 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin) |
36 | 3, 12, 4 | matbas2i 20594 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
37 | 1, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
38 | | elmapi 8143 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
40 | 39 | ad2antrr 719 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
41 | 22, 5 | symgbasf1o 18152 |
. . . . . . . . . 10
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁) |
42 | 41 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁) |
43 | | f1of 6377 |
. . . . . . . . 9
⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁) |
45 | 44 | ffvelrnda 6607 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁) |
46 | | simpr 479 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
47 | 40, 45, 46 | fovrnd 7065 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅)) |
48 | 47 | ralrimiva 3174 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑋𝑐) ∈ (Base‘𝑅)) |
49 | 28, 34, 35, 48 | gsummptcl 18718 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
50 | 12, 8 | ringcl 18914 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅)) |
51 | 25, 31, 49, 50 | syl3anc 1496 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∈ (Base‘𝑅)) |
52 | | disjdif 4262 |
. . . 4
⊢
((pmEven‘𝑁)
∩ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅ |
53 | 52 | a1i 11 |
. . 3
⊢ (𝜑 → ((pmEven‘𝑁) ∩
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ∅) |
54 | 22, 5 | evpmss 20290 |
. . . . . 6
⊢
(pmEven‘𝑁)
⊆ (Base‘(SymGrp‘𝑁)) |
55 | | undif 4271 |
. . . . . 6
⊢
((pmEven‘𝑁)
⊆ (Base‘(SymGrp‘𝑁)) ↔ ((pmEven‘𝑁) ∪ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) =
(Base‘(SymGrp‘𝑁))) |
56 | 54, 55 | mpbi 222 |
. . . . 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 18683 |
. 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 5685 |
. . . . . . 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 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑅 ∈ Ring) |
64 | 21 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑁 ∈ Fin) |
65 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (pmEven‘𝑁)) |
66 | | eqid 2824 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
67 | 6, 7, 66 | zrhpsgnevpm 20295 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅)) |
68 | 63, 64, 65, 67 | syl3anc 1496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (1r‘𝑅)) |
69 | 68 | oveq1d 6919 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
70 | 54 | sseli 3822 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (pmEven‘𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
71 | 70, 49 | sylan2 588 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
72 | 12, 8, 66 | ringlidm 18924 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
73 | 63, 71, 72 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((1r‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
74 | 69, 73 | eqtrd 2860 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
75 | 74 | mpteq2dva 4966 |
. . . . . 6
⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
76 | 62, 75 | syl5eq 2872 |
. . . . 5
⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
77 | 76 | oveq2d 6920 |
. . . 4
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
78 | | difss 3963 |
. . . . . . . 8
⊢
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁)) |
79 | | resmpt 5685 |
. . . . . . . 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 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑅 ∈ Ring) |
82 | 21 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑁 ∈ Fin) |
83 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
84 | | eqid 2824 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑅) = (invg‘𝑅) |
85 | 6, 7, 66, 5, 84 | zrhpsgnodpm 20296 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅))) |
86 | 81, 82, 83, 85 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) = ((invg‘𝑅)‘(1r‘𝑅))) |
87 | 86 | oveq1d 6919 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
88 | | eldifi 3958 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
89 | 88, 49 | sylan2 588 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
90 | 12, 8, 66, 84, 81, 89 | ringnegl 18947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
(((invg‘𝑅)‘(1r‘𝑅))(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
91 | 87, 90 | eqtrd 2860 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
92 | 91 | mpteq2dva 4966 |
. . . . . . . 8
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
93 | | eqidd 2825 |
. . . . . . . . 9
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
94 | | ringgrp 18905 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
95 | 16, 94 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Grp) |
96 | 12, 84 | grpinvf 17819 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Grp →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
98 | 97 | feqmptd 6495 |
. . . . . . . . 9
⊢ (𝜑 →
(invg‘𝑅) =
(𝑞 ∈ (Base‘𝑅) ↦
((invg‘𝑅)‘𝑞))) |
99 | | fveq2 6432 |
. . . . . . . . 9
⊢ (𝑞 = ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) → ((invg‘𝑅)‘𝑞) = ((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
100 | 89, 93, 98, 99 | fmptco 6645 |
. . . . . . . 8
⊢ (𝜑 →
((invg‘𝑅)
∘ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((invg‘𝑅)‘((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
101 | 92, 100 | eqtr4d 2863 |
. . . . . . 7
⊢ (𝜑 → (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
102 | 80, 101 | syl5eq 2872 |
. . . . . 6
⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) = ((invg‘𝑅) ∘ (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
103 | 102 | oveq2d 6920 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = (𝑅 Σg
((invg‘𝑅)
∘ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
104 | | mdetralt.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
105 | | ringabl 18933 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel) |
106 | 16, 105 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Abel) |
107 | | difssd 3964 |
. . . . . . 7
⊢ (𝜑 →
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))) |
108 | | ssfi 8448 |
. . . . . . 7
⊢
(((Base‘(SymGrp‘𝑁)) ∈ Fin ∧
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ⊆ (Base‘(SymGrp‘𝑁))) →
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin) |
109 | 24, 107, 108 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 →
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ∈ Fin) |
110 | | eqid 2824 |
. . . . . 6
⊢ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) = (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
111 | 12, 104, 84, 106, 109, 89, 110 | gsummptfidminv 18699 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg
((invg‘𝑅)
∘ (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
112 | 89 | ralrimiva 3174 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
113 | | mdetralt.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ 𝑁) |
114 | | mdetralt.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ 𝑁) |
115 | | prssi 4569 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → {𝐼, 𝐽} ⊆ 𝑁) |
116 | 113, 114,
115 | syl2anc 581 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ⊆ 𝑁) |
117 | | mdetralt.ij |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ≠ 𝐽) |
118 | | pr2nelem 9139 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o) |
119 | 113, 114,
117, 118 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ≈ 2o) |
120 | | eqid 2824 |
. . . . . . . . . . . 12
⊢
(pmTrsp‘𝑁) =
(pmTrsp‘𝑁) |
121 | | eqid 2824 |
. . . . . . . . . . . 12
⊢ ran
(pmTrsp‘𝑁) = ran
(pmTrsp‘𝑁) |
122 | 120, 121 | pmtrrn 18226 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) →
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
123 | 21, 116, 119, 122 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
124 | 22, 5, 121 | pmtrodpm 20302 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
125 | 21, 123, 124 | syl2anc 581 |
. . . . . . . . 9
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
126 | 22, 5 | evpmodpmf1o 20301 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
127 | 21, 125, 126 | syl2anc 581 |
. . . . . . . 8
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)):(pmEven‘𝑁)–1-1-onto→((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
128 | 12, 18, 109, 112, 110, 127 | gsummptfif1o 18719 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg ((𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))))) |
129 | | eleq1w 2888 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (𝑝 ∈ (pmEven‘𝑁) ↔ 𝑞 ∈ (pmEven‘𝑁))) |
130 | 129 | anbi2d 624 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ↔ (𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)))) |
131 | | oveq2 6912 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) |
132 | 131 | eleq1d 2890 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) |
133 | 130, 132 | imbi12d 336 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) ↔ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) |
134 | 22 | symggrp 18169 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ Fin →
(SymGrp‘𝑁) ∈
Grp) |
135 | 21, 134 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SymGrp‘𝑁) ∈ Grp) |
136 | 135 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (SymGrp‘𝑁) ∈ Grp) |
137 | 121, 22, 5 | symgtrf 18238 |
. . . . . . . . . . . . . 14
⊢ ran
(pmTrsp‘𝑁) ⊆
(Base‘(SymGrp‘𝑁)) |
138 | 123 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁)) |
139 | 137, 138 | sseldi 3824 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁))) |
140 | 70 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
141 | | eqid 2824 |
. . . . . . . . . . . . . 14
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
142 | 5, 141 | grpcl 17783 |
. . . . . . . . . . . . 13
⊢
(((SymGrp‘𝑁)
∈ Grp ∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁))) |
143 | 136, 139,
140, 142 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁))) |
144 | | eqid 2824 |
. . . . . . . . . . . . . . . . 17
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
145 | 22, 7, 144 | psgnghm2 20285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ Fin →
(pmSgn‘𝑁) ∈
((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
146 | 21, 145 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
147 | 146 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (pmSgn‘𝑁) ∈ ((SymGrp‘𝑁) GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
148 | | prex 5129 |
. . . . . . . . . . . . . . . 16
⊢ {1, -1}
∈ V |
149 | | eqid 2824 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
150 | | cnfldmul 20111 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
151 | 149, 150 | mgpplusg 18846 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
152 | 144, 151 | ressplusg 16351 |
. . . . . . . . . . . . . . . 16
⊢ ({1, -1}
∈ V → · =
(+g‘((mulGrp‘ℂfld) ↾s
{1, -1}))) |
153 | 148, 152 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ·
= (+g‘((mulGrp‘ℂfld)
↾s {1, -1})) |
154 | 5, 141, 153 | ghmlin 18015 |
. . . . . . . . . . . . . 14
⊢
(((pmSgn‘𝑁)
∈ ((SymGrp‘𝑁)
GrpHom ((mulGrp‘ℂfld) ↾s {1, -1}))
∧ ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝))) |
155 | 147, 139,
140, 154 | syl3anc 1496 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝))) |
156 | 22, 121, 7 | psgnpmtr 18280 |
. . . . . . . . . . . . . . . 16
⊢
(((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝑁) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1) |
157 | 138, 156 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) = -1) |
158 | 22, 5, 7 | psgnevpm 20293 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1) |
159 | 21, 158 | sylan 577 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘𝑝) = 1) |
160 | 157, 159 | oveq12d 6922 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = (-1 · 1)) |
161 | | neg1cn 11471 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
162 | 161 | mulid1i 10360 |
. . . . . . . . . . . . . 14
⊢ (-1
· 1) = -1 |
163 | 160, 162 | syl6eq 2876 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmSgn‘𝑁)‘((pmTrsp‘𝑁)‘{𝐼, 𝐽})) · ((pmSgn‘𝑁)‘𝑝)) = -1) |
164 | 155, 163 | eqtrd 2860 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) |
165 | 22, 5, 7 | psgnodpmr 20294 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧
(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ (Base‘(SymGrp‘𝑁)) ∧ ((pmSgn‘𝑁)‘(((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) = -1) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
166 | 64, 143, 164, 165 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
167 | 133, 166 | chvarv 2416 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ (pmEven‘𝑁)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) |
168 | | eqidd 2825 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)) = (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) |
169 | | fveq1 6431 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑝‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)) |
170 | 169 | oveq1d 6919 |
. . . . . . . . . . . 12
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((𝑝‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) |
171 | 170 | mpteq2dv 4967 |
. . . . . . . . . . 11
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) |
172 | 171 | oveq2d 6920 |
. . . . . . . . . 10
⊢ (𝑝 = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) |
173 | 167, 168,
93, 172 | fmptco 6645 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))))) |
174 | | oveq2 6912 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑝 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)) |
175 | 174 | fveq1d 6434 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑝 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)) |
176 | 175 | oveq1d 6919 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑝 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐) = (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) |
177 | 176 | mpteq2dv 4967 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) |
178 | 177 | oveq2d 6920 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) |
179 | 178 | cbvmptv 4972 |
. . . . . . . . . 10
⊢ (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) |
180 | 179 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑞 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))))) |
181 | 139 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁))) |
182 | 140 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑝 ∈ (Base‘(SymGrp‘𝑁))) |
183 | 22, 5, 141 | symgov 18159 |
. . . . . . . . . . . . . . . . 17
⊢
((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)) |
184 | 181, 182,
183 | syl2anc 581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)) |
185 | 184 | fveq1d 6434 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐)) |
186 | 70, 44 | sylan2 588 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → 𝑝:𝑁⟶𝑁) |
187 | | fvco3 6521 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝:𝑁⟶𝑁 ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
188 | 186, 187 | sylan 577 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∘ 𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
189 | 185, 188 | eqtrd 2860 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))) |
190 | 189 | oveq1d 6919 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐)) |
191 | 120 | pmtrprfv 18222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
192 | 21, 113, 114, 117, 191 | syl13anc 1497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
193 | 192 | ad2antrr 719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼) = 𝐽) |
194 | 193 | oveq1d 6919 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐽𝑋𝑐)) |
195 | | oveq2 6912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝐼𝑋𝑎) = (𝐼𝑋𝑐)) |
196 | | oveq2 6912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝐽𝑋𝑎) = (𝐽𝑋𝑐)) |
197 | 195, 196 | eqeq12d 2839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → ((𝐼𝑋𝑎) = (𝐽𝑋𝑎) ↔ (𝐼𝑋𝑐) = (𝐽𝑋𝑐))) |
198 | | mdetralt.eq |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎)) |
199 | 198 | ad2antrr 719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎)) |
200 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
201 | 197, 199,
200 | rspcdva 3531 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝐼𝑋𝑐) = (𝐽𝑋𝑐)) |
202 | 194, 201 | eqtr4d 2863 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐)) |
203 | | fveq2 6432 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝‘𝑐) = 𝐼 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)) |
204 | 203 | oveq1d 6919 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐)) |
205 | | oveq1 6911 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝‘𝑐) = 𝐼 → ((𝑝‘𝑐)𝑋𝑐) = (𝐼𝑋𝑐)) |
206 | 204, 205 | eqeq12d 2839 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝‘𝑐) = 𝐼 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐼)𝑋𝑐) = (𝐼𝑋𝑐))) |
207 | 202, 206 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
208 | | prcom 4484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝐼, 𝐽} = {𝐽, 𝐼} |
209 | 208 | fveq2i 6435 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((pmTrsp‘𝑁)‘{𝐼, 𝐽}) = ((pmTrsp‘𝑁)‘{𝐽, 𝐼}) |
210 | 209 | fveq1i 6433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) |
211 | 117 | necomd 3053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
212 | 120 | pmtrprfv 18222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ (𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼)) → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼) |
213 | 21, 114, 113, 211, 212 | syl13anc 1497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐽, 𝐼})‘𝐽) = 𝐼) |
214 | 210, 213 | syl5eq 2872 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽) = 𝐼) |
215 | 214 | oveq1d 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐)) |
216 | 215 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐼𝑋𝑐)) |
217 | 216, 201 | eqtrd 2860 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐)) |
218 | | fveq2 6432 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘𝑐) = 𝐽 → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)) |
219 | 218 | oveq1d 6919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐)) |
220 | | oveq1 6911 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐)𝑋𝑐) = (𝐽𝑋𝑐)) |
221 | 219, 220 | eqeq12d 2839 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝‘𝑐) = 𝐽 → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐) ↔ ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘𝐽)𝑋𝑐) = (𝐽𝑋𝑐))) |
222 | 217, 221 | syl5ibrcom 239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
223 | 222 | a1dd 50 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) = 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))) |
224 | | neanior 3090 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) ↔ ¬ ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼)) |
225 | | elpri 4418 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐼 ∨ (𝑝‘𝑐) = 𝐽)) |
226 | 225 | orcomd 904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝‘𝑐) ∈ {𝐼, 𝐽} → ((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼)) |
227 | 226 | con3i 152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
((𝑝‘𝑐) = 𝐽 ∨ (𝑝‘𝑐) = 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
228 | 224, 227 | sylbi 209 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
229 | 228 | 3adant1 1166 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ {𝐼, 𝐽}) |
230 | 120 | pmtrmvd 18225 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) → dom
(((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
231 | 21, 116, 119, 230 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
232 | 231 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
233 | 232 | 3ad2ant1 1169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) = {𝐼, 𝐽}) |
234 | 229, 233 | neleqtrrd 2927 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I )) |
235 | 120 | pmtrf 18224 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ Fin ∧ {𝐼, 𝐽} ⊆ 𝑁 ∧ {𝐼, 𝐽} ≈ 2o) →
((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁) |
236 | 21, 116, 119, 235 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}):𝑁⟶𝑁) |
237 | 236 | ffnd 6278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁) |
238 | 237 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁) |
239 | 186 | ffvelrnda 6607 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁) |
240 | | fnelnfp 6694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((pmTrsp‘𝑁)‘{𝐼, 𝐽}) Fn 𝑁 ∧ (𝑝‘𝑐) ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
241 | 238, 239,
240 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
242 | 241 | 3ad2ant1 1169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) ≠ (𝑝‘𝑐))) |
243 | 242 | necon2bbid 3041 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐) ↔ ¬ (𝑝‘𝑐) ∈ dom (((pmTrsp‘𝑁)‘{𝐼, 𝐽}) ∖ I ))) |
244 | 234, 243 | mpbird 249 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → (((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐)) = (𝑝‘𝑐)) |
245 | 244 | oveq1d 6919 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) ∧ (𝑝‘𝑐) ≠ 𝐽 ∧ (𝑝‘𝑐) ≠ 𝐼) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
246 | 245 | 3exp 1154 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐽 → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)))) |
247 | 223, 246 | pm2.61dne 3084 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐) ≠ 𝐼 → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐))) |
248 | 207, 247 | pm2.61dne 3084 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝐼, 𝐽})‘(𝑝‘𝑐))𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
249 | 190, 248 | eqtrd 2860 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) ∧ 𝑐 ∈ 𝑁) → (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐) = ((𝑝‘𝑐)𝑋𝑐)) |
250 | 249 | mpteq2dva 4966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)) = (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) |
251 | 250 | oveq2d 6920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (pmEven‘𝑁)) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐))) = ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) |
252 | 251 | mpteq2dva 4966 |
. . . . . . . . 9
⊢ (𝜑 → (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ (((((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑝)‘𝑐)𝑋𝑐)))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
253 | 173, 180,
252 | 3eqtrd 2864 |
. . . . . . . 8
⊢ (𝜑 → ((𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞))) = (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) |
254 | 253 | oveq2d 6920 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))) ∘ (𝑞 ∈ (pmEven‘𝑁) ↦ (((pmTrsp‘𝑁)‘{𝐼, 𝐽})(+g‘(SymGrp‘𝑁))𝑞)))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
255 | 128, 254 | eqtrd 2860 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) = (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) |
256 | 255 | fveq2d 6436 |
. . . . 5
⊢ (𝜑 →
((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)) ↦ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
257 | 103, 111,
256 | 3eqtrd 2864 |
. . . 4
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))) = ((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) |
258 | 77, 257 | oveq12d 6922 |
. . 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
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))))) |
259 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (pmEven‘𝑁) ⊆
(Base‘(SymGrp‘𝑁))) |
260 | | ssfi 8448 |
. . . . . 6
⊢
(((Base‘(SymGrp‘𝑁)) ∈ Fin ∧ (pmEven‘𝑁) ⊆
(Base‘(SymGrp‘𝑁))) → (pmEven‘𝑁) ∈ Fin) |
261 | 24, 259, 260 | syl2anc 581 |
. . . . 5
⊢ (𝜑 → (pmEven‘𝑁) ∈ Fin) |
262 | 71 | ralrimiva 3174 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ (pmEven‘𝑁)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))) ∈ (Base‘𝑅)) |
263 | 12, 18, 261, 262 | gsummptcl 18718 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) |
264 | 12, 13, 104, 84 | grprinv 17822 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝑅 Σg
(𝑝 ∈
(pmEven‘𝑁) ↦
((mulGrp‘𝑅)
Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ∈ (Base‘𝑅)) → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 ) |
265 | 95, 263, 264 | syl2anc 581 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐)))))(+g‘𝑅)((invg‘𝑅)‘(𝑅 Σg (𝑝 ∈ (pmEven‘𝑁) ↦ ((mulGrp‘𝑅) Σg
(𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))))) = 0 ) |
266 | 258, 265 | eqtrd 2860 |
. 2
⊢ (𝜑 → ((𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾ (pmEven‘𝑁)))(+g‘𝑅)(𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑋𝑐))))) ↾
((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))))) = 0 ) |
267 | 11, 60, 266 | 3eqtrd 2864 |
1
⊢ (𝜑 → (𝐷‘𝑋) = 0 ) |