Step |
Hyp |
Ref |
Expression |
1 |
|
dchrmhm.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
2 |
|
dchrmhm.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
3 |
|
dchrmhm.b |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
4 |
|
dchrmul.t |
⊢ · = ( +g ‘ 𝐺 ) |
5 |
|
dchrplusg.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
7 |
|
eqid |
⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 ) |
8 |
1 2 6 7 5 3
|
dchrbas |
⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 } ) |
9 |
1 2 6 7 5 8
|
dchrval |
⊢ ( 𝜑 → 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } ) |
10 |
9
|
fveq2d |
⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } ) ) |
11 |
3
|
fvexi |
⊢ 𝐷 ∈ V |
12 |
11 11
|
xpex |
⊢ ( 𝐷 × 𝐷 ) ∈ V |
13 |
|
ofexg |
⊢ ( ( 𝐷 × 𝐷 ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V ) |
14 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } = { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } |
15 |
14
|
grpplusg |
⊢ ( ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } ) ) |
16 |
12 13 15
|
mp2b |
⊢ ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , 𝐷 〉 , 〈 ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) 〉 } ) |
17 |
10 4 16
|
3eqtr4g |
⊢ ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ) |