Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. 2
⊢ 𝐺 = (DChr‘𝑁) |
2 | | df-dchr 24958 |
. . . 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 | | fvexd 6203 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
(ℤ/nℤ‘𝑛) ∈ V) |
5 | | ovex 6678 |
. . . . . . 7
⊢
((mulGrp‘𝑧)
MndHom (mulGrp‘ℂfld)) ∈ V |
6 | 5 | rabex 4813 |
. . . . . 6
⊢ {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} ∈ V |
7 | 6 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} ∈ V) |
8 | | dchrval.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
9 | 8 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
10 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
11 | 10 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
(ℤ/nℤ‘𝑛) = (ℤ/nℤ‘𝑁)) |
12 | | dchrval.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
13 | 11, 12 | syl6reqr 2675 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑍 = (ℤ/nℤ‘𝑛)) |
14 | 13 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (𝑧 = 𝑍 ↔ 𝑧 = (ℤ/nℤ‘𝑛))) |
15 | 14 | biimpar 502 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝑧 = 𝑍) |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (mulGrp‘𝑧) = (mulGrp‘𝑍)) |
17 | 16 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) = ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
18 | 15 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Base‘𝑧) = (Base‘𝑍)) |
19 | | dchrval.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑍) |
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Base‘𝑧) = 𝐵) |
21 | 15 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Unit‘𝑧) = (Unit‘𝑍)) |
22 | | dchrval.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑍) |
23 | 21, 22 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (Unit‘𝑧) = 𝑈) |
24 | 20, 23 | difeq12d 3729 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((Base‘𝑧) ∖ (Unit‘𝑧)) = (𝐵 ∖ 𝑈)) |
25 | 24 | xpeq1d 5138 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) = ((𝐵 ∖ 𝑈) × {0})) |
26 | 25 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ((((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥 ↔ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥)) |
27 | 17, 26 | rabeqbidv 3195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} = {𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) |
28 | 9, 27 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) |
29 | 28 | eqeq2d 2632 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → (𝑏 = 𝐷 ↔ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥})) |
30 | 29 | biimpar 502 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 𝑏 = 𝐷) |
31 | 30 | opeq2d 4409 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐷〉) |
32 | 30 | sqxpeqd 5141 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → (𝑏 × 𝑏) = (𝐷 × 𝐷)) |
33 | 32 | reseq2d 5396 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → ( ∘𝑓
· ↾ (𝑏 ×
𝑏)) = (
∘𝑓 · ↾ (𝐷 × 𝐷))) |
34 | 33 | opeq2d 4409 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → 〈(+g‘ndx), (
∘𝑓 · ↾ (𝑏 × 𝑏))〉 = 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉) |
35 | 31, 34 | preq12d 4276 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) ∧ 𝑏 = {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
36 | 7, 35 | csbied 3560 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑧 = (ℤ/nℤ‘𝑛)) → ⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
37 | 4, 36 | csbied 3560 |
. . 3
⊢ ((𝜑 ∧ 𝑛 = 𝑁) →
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝑏 × 𝑏))〉} =
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉}) |
38 | | dchrval.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
39 | | prex 4909 |
. . . 4
⊢
{〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), (
∘𝑓 · ↾ (𝐷 × 𝐷))〉} ∈ V |
40 | 39 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉} ∈
V) |
41 | 3, 37, 38, 40 | fvmptd 6288 |
. 2
⊢ (𝜑 → (DChr‘𝑁) = {〈(Base‘ndx),
𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉}) |
42 | 1, 41 | syl5eq 2668 |
1
⊢ (𝜑 → 𝐺 = {〈(Base‘ndx), 𝐷〉,
〈(+g‘ndx), ( ∘𝑓 · ↾
(𝐷 × 𝐷))〉}) |