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 24761 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋))) |
8 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
9 | 8, 3 | mgpbas 18318 |
. . . . . . . . . 10
⊢ 𝐵 =
(Base‘(mulGrp‘𝑍)) |
10 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
11 | | cnfldbas 19571 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
12 | 10, 11 | mgpbas 18318 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
13 | 9, 12 | mhmf 17163 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → 𝑋:𝐵⟶ℂ) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → 𝑋:𝐵⟶ℂ) |
15 | | ffun 5961 |
. . . . . . . 8
⊢ (𝑋:𝐵⟶ℂ → Fun 𝑋) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → Fun 𝑋) |
17 | | funssres 5844 |
. . . . . . 7
⊢ ((Fun
𝑋 ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
18 | 16, 17 | sylan 487 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
19 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) |
20 | | resss 5342 |
. . . . . . 7
⊢ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) ⊆ 𝑋 |
21 | 19, 20 | syl6eqssr 3619 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0})) → ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) |
22 | 18, 21 | impbida 873 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋 ↔ (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0}))) |
23 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
24 | | fconst6g 6007 |
. . . . . . . . 9
⊢ (0 ∈
ℂ → ((𝐵 ∖
𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ) |
25 | 23, 24 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝐵 ∖ 𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ) |
26 | | fdm 5964 |
. . . . . . . 8
⊢ (((𝐵 ∖ 𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ → dom ((𝐵 ∖ 𝑈) × {0}) = (𝐵 ∖ 𝑈)) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → dom ((𝐵 ∖ 𝑈) × {0}) = (𝐵 ∖ 𝑈)) |
28 | 27 | reseq2d 5317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = (𝑋 ↾ (𝐵 ∖ 𝑈))) |
29 | 28 | eqeq1d 2612 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ dom ((𝐵 ∖ 𝑈) × {0})) = ((𝐵 ∖ 𝑈) × {0}) ↔ (𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}))) |
30 | 22, 29 | bitrd 267 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋 ↔ (𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}))) |
31 | | difss 3699 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝑈) ⊆ 𝐵 |
32 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝑋:𝐵⟶ℂ ∧ (𝐵 ∖ 𝑈) ⊆ 𝐵) → (𝑋 ↾ (𝐵 ∖ 𝑈)):(𝐵 ∖ 𝑈)⟶ℂ) |
33 | 14, 31, 32 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ (𝐵 ∖ 𝑈)):(𝐵 ∖ 𝑈)⟶ℂ) |
34 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑋 ↾ (𝐵 ∖ 𝑈)):(𝐵 ∖ 𝑈)⟶ℂ → (𝑋 ↾ (𝐵 ∖ 𝑈)) Fn (𝐵 ∖ 𝑈)) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (𝑋 ↾ (𝐵 ∖ 𝑈)) Fn (𝐵 ∖ 𝑈)) |
36 | | ffn 5958 |
. . . . . . 7
⊢ (((𝐵 ∖ 𝑈) × {0}):(𝐵 ∖ 𝑈)⟶ℂ → ((𝐵 ∖ 𝑈) × {0}) Fn (𝐵 ∖ 𝑈)) |
37 | 25, 36 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝐵 ∖ 𝑈) × {0}) Fn (𝐵 ∖ 𝑈)) |
38 | | eqfnfv 6219 |
. . . . . 6
⊢ (((𝑋 ↾ (𝐵 ∖ 𝑈)) Fn (𝐵 ∖ 𝑈) ∧ ((𝐵 ∖ 𝑈) × {0}) Fn (𝐵 ∖ 𝑈)) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥))) |
39 | 35, 37, 38 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥))) |
40 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → ((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (𝑋‘𝑥)) |
41 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
42 | 41 | fvconst2 6374 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → (((𝐵 ∖ 𝑈) × {0})‘𝑥) = 0) |
43 | 40, 42 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) → (((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ (𝑋‘𝑥) = 0)) |
44 | 43 | ralbiia 2962 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝑈)(𝑋‘𝑥) = 0) |
45 | | eldif 3550 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ 𝑈) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈)) |
46 | 45 | imbi1i 338 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐵 ∖ 𝑈) → (𝑋‘𝑥) = 0) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) = 0)) |
47 | | impexp 461 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) = 0) ↔ (𝑥 ∈ 𝐵 → (¬ 𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0))) |
48 | | con1b 347 |
. . . . . . . . . 10
⊢ ((¬
𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0) ↔ (¬ (𝑋‘𝑥) = 0 → 𝑥 ∈ 𝑈)) |
49 | | df-ne 2782 |
. . . . . . . . . . 11
⊢ ((𝑋‘𝑥) ≠ 0 ↔ ¬ (𝑋‘𝑥) = 0) |
50 | 49 | imbi1i 338 |
. . . . . . . . . 10
⊢ (((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ↔ (¬ (𝑋‘𝑥) = 0 → 𝑥 ∈ 𝑈)) |
51 | 48, 50 | bitr4i 266 |
. . . . . . . . 9
⊢ ((¬
𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0) ↔ ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
52 | 51 | imbi2i 325 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 → (¬ 𝑥 ∈ 𝑈 → (𝑋‘𝑥) = 0)) ↔ (𝑥 ∈ 𝐵 → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
53 | 46, 47, 52 | 3bitri 285 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∖ 𝑈) → (𝑋‘𝑥) = 0) ↔ (𝑥 ∈ 𝐵 → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
54 | 53 | ralbii2 2961 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)(𝑋‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
55 | 44, 54 | bitri 263 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝑈)((𝑋 ↾ (𝐵 ∖ 𝑈))‘𝑥) = (((𝐵 ∖ 𝑈) × {0})‘𝑥) ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
56 | 39, 55 | syl6bb 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → ((𝑋 ↾ (𝐵 ∖ 𝑈)) = ((𝐵 ∖ 𝑈) × {0}) ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
57 | 30, 56 | bitrd 267 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
58 | 57 | pm5.32da 671 |
. 2
⊢ (𝜑 → ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋) ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |
59 | 7, 58 | bitrd 267 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |