Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. 2
⊢ 𝐺 = (DChr‘𝑁) |
2 | | df-dchr 24758 |
. . . 4
⊢ DChr =
(𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉}) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → DChr = (𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉})) |
4 | | fvex 6113 |
. . . . 5
⊢
(ℤ/nℤ‘𝑛) ∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
(ℤ/nℤ‘𝑛) ∈ V) |
6 | | ovex 6577 |
. . . . . . 7
⊢
((mulGrp‘𝑧)
MndHom (mulGrp‘ℂfld)) ∈ V |
7 | 6 | rabex 4740 |
. . . . . 6
⊢ {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} ∈ V) |
9 | | dchrval.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
10 | 9 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
11 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
(ℤ/nℤ‘𝑛) = (ℤ/nℤ‘𝑁)) |
13 | | dchrval.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
14 | 12, 13 | syl6reqr 2663 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑍 = (ℤ/nℤ‘𝑛)) |
15 | 14 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (𝑧 = 𝑍 ↔ 𝑧 = (ℤ/nℤ‘𝑛))) |
16 | 15 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝑧 = 𝑍) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (mulGrp‘𝑧) = (mulGrp‘𝑍)) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) = ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
19 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Base‘𝑧) = (Base‘𝑍)) |
20 | | dchrval.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑍) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Base‘𝑧) = 𝐵) |
22 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Unit‘𝑧) = (Unit‘𝑍)) |
23 | | dchrval.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑍) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Unit‘𝑧) = 𝑈) |
25 | 21, 24 | difeq12d 3691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((Base‘𝑧) ∖ (Unit‘𝑧)) = (𝐵 ∖ 𝑈)) |
26 | 25 | xpeq1d 5062 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) = ((𝐵 ∖ 𝑈) × {0})) |
27 | 26 | sseq1d 3595 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥 ↔ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥)) |
28 | 18, 27 | rabeqbidv 3168 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
29 | 10, 28 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) |
30 | 29 | eqeq2d 2620 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (𝑏 = 𝐷 ↔ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥})) |
31 | 30 | biimpar 501 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 𝑏 = 𝐷) |
32 | 31 | opeq2d 4347 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐷〉) |
33 | 31 | sqxpeqd 5065 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → (𝑏 × 𝑏) = (𝐷 × 𝐷)) |
34 | 33 | reseq2d 5317 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → ( ∘𝑓
· ↾ (𝑏 ×
𝑏)) = (
∘𝑓 · ↾ (𝐷 × 𝐷))) |
35 | 34 | opeq2d 4347 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 〈(+g‘ndx), (
∘𝑓 · ↾ (𝑏 × 𝑏))〉 = 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉) |
36 | 32, 35 | preq12d 4220 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
37 | 8, 36 | csbied 3526 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
38 | 5, 37 | csbied 3526 |
. . 3
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
39 | | dchrval.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
40 | | prex 4836 |
. . . 4
⊢
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉} ∈ V |
41 | 40 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉} ∈
V) |
42 | 3, 38, 39, 41 | fvmptd 6197 |
. 2
⊢ (𝜑 → (DChr‘𝑁) = {〈(Base‘ndx),
𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉}) |
43 | 1, 42 | syl5eq 2656 |
1
⊢ (𝜑 → 𝐺 = {〈(Base‘ndx), 𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉}) |