Step |
Hyp |
Ref |
Expression |
1 |
|
dchrmhm.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
2 |
|
dchrmhm.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
3 |
|
dchrmhm.b |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
5 |
|
eqid |
⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 ) |
6 |
1 3
|
dchrrcl |
⊢ ( 𝑥 ∈ 𝐷 → 𝑁 ∈ ℕ ) |
7 |
1 2 4 5 6 3
|
dchrelbas |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) ) ) |
8 |
7
|
ibi |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) ) |
9 |
8
|
simpld |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) |
10 |
9
|
ssriv |
⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) |