Proof of Theorem dchrelbas2
Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
2 | | dchrval.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | dchrval.b |
. . 3
⊢ 𝐵 = (Base‘𝑍) |
4 | | dchrval.u |
. . 3
⊢ 𝑈 = (Unit‘𝑍) |
5 | | dchrval.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | dchrbas.b |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
7 | 1, 2, 3, 4, 5, 6 | dchrelbas 25985 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋))) |
8 | | eqid 2739 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
9 | 8, 3 | mgpbas 19377 |
. . . . . . . . 9
⊢ 𝐵 =
(Base‘(mulGrp‘𝑍)) |
10 | | eqid 2739 |
. . . . . . . . . 10
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
11 | | cnfldbas 20234 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘ℂfld) |
12 | 10, 11 | mgpbas 19377 |
. . . . . . . . 9
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
13 | 9, 12 | mhmf 18090 |
. . . . . . . 8
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → 𝑋:𝐵⟶ℂ) |
14 | 13 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → 𝑋:𝐵⟶ℂ) |
15 | 14 | ffund 6519 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → Fun 𝑋) |
16 | | funssres 6394 |
. . . . . 6
⊢ ((Fun
𝑋 ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
17 | 15, 16 | sylan 583 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
18 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
19 | | resss 5860 |
. . . . . 6
⊢ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) ⊆ 𝑋 |
20 | 18, 19 | eqsstrrdi 3942 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) → ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) |
21 | 17, 20 | impbida 801 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋 ↔ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0}))) |
22 | | 0cn 10724 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
23 | | fconst6g 6578 |
. . . . . . . 8
⊢ (0 ∈
ℂ → ((𝐵 ∖
𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝐵 ∖ 𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ) |
25 | 24 | fdmd 6526 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → dom ((𝐵 ∖ 𝑈) × {0}) = (𝐵 ∖ 𝑈)) |
26 | 25 | reseq2d 5835 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = (𝑋 ↾ (𝐵 ∖ 𝑈))) |
27 | 26 | eqeq1d 2741 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0}) ↔ (𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}))) |
28 | | difss 4032 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝑈) ⊆ 𝐵 |
29 | | fssres 6555 |
. . . . . . . 8
⊢ ((𝑋:𝐵⟶ℂ ∧ (𝐵 ∖ 𝑈) ⊆ 𝐵) → (𝑋 ↾ (𝐵 ∖ 𝑈)):(𝐵 ∖ 𝑈)⟶ℂ) |
30 | 14, 28, 29 | sylancl 589 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ (𝐵 ∖ 𝑈)):(𝐵 ∖ 𝑈)⟶ℂ) |
31 | 30 | ffnd 6516 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ (𝐵 ∖ 𝑈)) Fn (𝐵 ∖ 𝑈)) |
32 | 24 | ffnd 6516 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝐵 ∖ 𝑈) × {0}) Fn (𝐵 ∖ 𝑈)) |
33 | | eqfnfv 6822 |
. . . . . 6
⊢ (((𝑋 ↾ (𝐵 ∖ 𝑈)) Fn (𝐵 ∖ 𝑈) ∧ ((𝐵 ∖ 𝑈) × {0}) Fn (𝐵 ∖ 𝑈)) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥))) |
34 | 31, 32, 33 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥))) |
35 | | fvres 6706 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → ((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (𝑋‘𝑥)) |
36 | | c0ex 10726 |
. . . . . . . . 9
⊢ 0 ∈
V |
37 | 36 | fvconst2 6989 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → (((𝐵 ∖ 𝑈) × {0})‘𝑥) = 0) |
38 | 35, 37 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → (((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ (𝑋‘𝑥) = 0)) |
39 | 38 | ralbiia 3080 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)(𝑋‘𝑥) = 0) |
40 | | eldif 3863 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈)) |
41 | 40 | imbi1i 353 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐵 ∖ 𝑈) → (𝑋‘𝑥) = 0) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) = 0)) |
42 | | impexp 454 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) = 0) ↔ (𝑥 ∈ 𝐵 → (¬ 𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0))) |
43 | | con1b 362 |
. . . . . . . . . 10
⊢ ((¬
𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0) ↔ (¬ (𝑋‘𝑥) = 0 → 𝑥 ∈ 𝑈)) |
44 | | df-ne 2936 |
. . . . . . . . . . 11
⊢ ((𝑋‘𝑥) ≠ 0 ↔ ¬ (𝑋‘𝑥) = 0) |
45 | 44 | imbi1i 353 |
. . . . . . . . . 10
⊢ (((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ↔ (¬ (𝑋‘𝑥) = 0 → 𝑥 ∈ 𝑈)) |
46 | 43, 45 | bitr4i 281 |
. . . . . . . . 9
⊢ ((¬
𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0) ↔ ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
47 | 46 | imbi2i 339 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 → (¬ 𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0)) ↔ (𝑥 ∈ 𝐵 → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
48 | 41, 42, 47 | 3bitri 300 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∖ 𝑈) → (𝑋‘𝑥) = 0) ↔ (𝑥 ∈ 𝐵 → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
49 | 48 | ralbii2 3079 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)(𝑋‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
50 | 39, 49 | bitri 278 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
51 | 34, 50 | bitrdi 290 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
52 | 21, 27, 51 | 3bitrd 308 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
53 | 52 | pm5.32da 582 |
. 2
⊢ (𝜑 → ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |
54 | 7, 53 | bitrd 282 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |