Step | Hyp | Ref
| Expression |
1 | | dchrpt.g |
. . . . 5
⊢ 𝐺 = (DChr‘𝑁) |
2 | | dchrpt.z |
. . . . 5
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | dchrpt.d |
. . . . 5
⊢ 𝐷 = (Base‘𝐺) |
4 | | dchrpt.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑍) |
5 | | dchrpt.1 |
. . . . 5
⊢ 1 =
(1r‘𝑍) |
6 | | dchrpt.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
7 | 6 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → 𝑁 ∈ ℕ) |
8 | | dchrpt.n1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 1 ) |
9 | 8 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → 𝐴 ≠ 1 ) |
10 | | eqid 2739 |
. . . . 5
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
11 | | eqid 2739 |
. . . . 5
⊢
((mulGrp‘𝑍)
↾s (Unit‘𝑍)) = ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) |
12 | | eqid 2739 |
. . . . 5
⊢
(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) =
(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) |
13 | | oveq1 7241 |
. . . . . . . . 9
⊢ (𝑛 = 𝑏 → (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)) = (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) |
14 | 13 | cbvmptv 5174 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) |
15 | | fveq2 6738 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑎 → (𝑤‘𝑘) = (𝑤‘𝑎)) |
16 | 15 | oveq2d 7250 |
. . . . . . . . 9
⊢ (𝑘 = 𝑎 → (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)) = (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑎))) |
17 | 16 | mpteq2dv 5167 |
. . . . . . . 8
⊢ (𝑘 = 𝑎 → (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑎)))) |
18 | 14, 17 | syl5eq 2792 |
. . . . . . 7
⊢ (𝑘 = 𝑎 → (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑎)))) |
19 | 18 | rneqd 5824 |
. . . . . 6
⊢ (𝑘 = 𝑎 → ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))) = ran (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑎)))) |
20 | 19 | cbvmptv 5174 |
. . . . 5
⊢ (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) = (𝑎 ∈ dom 𝑤 ↦ ran (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑎)))) |
21 | | simpllr 776 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → 𝐴 ∈ (Unit‘𝑍)) |
22 | | simplr 769 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → 𝑤 ∈ Word (Unit‘𝑍)) |
23 | | simprl 771 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → ((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) |
24 | | simprr 773 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍)) |
25 | 1, 2, 3, 4, 5, 7, 9, 10, 11, 12, 20, 21, 22, 23, 24 | dchrptlem3 26176 |
. . . 4
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
26 | 25 | 3adantr1 1171 |
. . 3
⊢ ((((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ ((𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))):dom 𝑤⟶{𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍))) ∣
(((mulGrp‘𝑍)
↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} ∧
((mulGrp‘𝑍)
↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
27 | 10, 11 | unitgrpbas 19714 |
. . . 4
⊢
(Unit‘𝑍) =
(Base‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) |
28 | | eqid 2739 |
. . . 4
⊢ {𝑢 ∈
(SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣
(((mulGrp‘𝑍)
↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} = {𝑢 ∈
(SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣
(((mulGrp‘𝑍)
↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp
)} |
29 | 6 | nnnn0d 12177 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
30 | 2 | zncrng 20539 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
31 | 10, 11 | unitabl 19716 |
. . . . . 6
⊢ (𝑍 ∈ CRing →
((mulGrp‘𝑍)
↾s (Unit‘𝑍)) ∈ Abel) |
32 | 29, 30, 31 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑍) ↾s
(Unit‘𝑍)) ∈
Abel) |
33 | 32 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) → ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ∈ Abel) |
34 | 2, 4 | znfi 20554 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) |
35 | 6, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) |
36 | 4, 10 | unitss 19708 |
. . . . . 6
⊢
(Unit‘𝑍)
⊆ 𝐵 |
37 | | ssfi 8876 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧
(Unit‘𝑍) ⊆
𝐵) → (Unit‘𝑍) ∈ Fin) |
38 | 35, 36, 37 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (Unit‘𝑍) ∈ Fin) |
39 | 38 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) → (Unit‘𝑍) ∈ Fin) |
40 | | eqid 2739 |
. . . 4
⊢ (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) |
41 | 27, 28, 33, 39, 12, 40 | ablfac2 19506 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) → ∃𝑤 ∈ Word (Unit‘𝑍)((𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))):dom 𝑤⟶{𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍))) ∣
(((mulGrp‘𝑍)
↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} ∧
((mulGrp‘𝑍)
↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s
(Unit‘𝑍)))(𝑤‘𝑘))))) = (Unit‘𝑍))) |
42 | 26, 41 | r19.29a 3217 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (Unit‘𝑍)) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
43 | 1 | dchrabl 26164 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
44 | | ablgrp 19205 |
. . . 4
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
45 | | eqid 2739 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
46 | 3, 45 | grpidcl 18425 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐷) |
47 | 6, 43, 44, 46 | 4syl 19 |
. . 3
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐷) |
48 | | 0ne1 11928 |
. . . 4
⊢ 0 ≠
1 |
49 | | dchrpt.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
50 | 1, 2, 3, 4, 10, 47, 49 | dchrn0 26160 |
. . . . . . 7
⊢ (𝜑 →
(((0g‘𝐺)‘𝐴) ≠ 0 ↔ 𝐴 ∈ (Unit‘𝑍))) |
51 | 50 | necon1bbid 2982 |
. . . . . 6
⊢ (𝜑 → (¬ 𝐴 ∈ (Unit‘𝑍) ↔ ((0g‘𝐺)‘𝐴) = 0)) |
52 | 51 | biimpa 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ((0g‘𝐺)‘𝐴) = 0) |
53 | 52 | neeq1d 3002 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → (((0g‘𝐺)‘𝐴) ≠ 1 ↔ 0 ≠ 1)) |
54 | 48, 53 | mpbiri 261 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ((0g‘𝐺)‘𝐴) ≠ 1) |
55 | | fveq1 6737 |
. . . . 5
⊢ (𝑥 = (0g‘𝐺) → (𝑥‘𝐴) = ((0g‘𝐺)‘𝐴)) |
56 | 55 | neeq1d 3002 |
. . . 4
⊢ (𝑥 = (0g‘𝐺) → ((𝑥‘𝐴) ≠ 1 ↔ ((0g‘𝐺)‘𝐴) ≠ 1)) |
57 | 56 | rspcev 3551 |
. . 3
⊢
(((0g‘𝐺) ∈ 𝐷 ∧ ((0g‘𝐺)‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
58 | 47, 54, 57 | syl2an2r 685 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
59 | 42, 58 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |