Step |
Hyp |
Ref |
Expression |
1 |
|
dchrval.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
2 |
|
dchrval.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
3 |
|
dchrval.b |
⊢ 𝐵 = ( Base ‘ 𝑍 ) |
4 |
|
dchrval.u |
⊢ 𝑈 = ( Unit ‘ 𝑍 ) |
5 |
|
dchrval.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
6 |
|
dchrbas.b |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
7 |
1 2 3 4 5 6
|
dchrbas |
⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) |
8 |
7
|
eleq2d |
⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ 𝑋 ∈ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) ) |
9 |
|
sseq2 |
⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 ↔ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) |
10 |
9
|
elrab |
⊢ ( 𝑋 ∈ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) |
11 |
8 10
|
bitrdi |
⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) ) |