Metamath Proof Explorer

Theorem dchrinv

Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrabs.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrabs.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrabs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion dchrinv ( 𝜑 → ( 𝐼 ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dchrabs.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrabs.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 dchrabs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
4 dchrinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 cjf ⊢ ∗ : ℂ ⟶ ℂ
8 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
9 1 5 2 8 3 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
10 fco ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ) → ( ∗ ∘ 𝑋 ) : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
11 7 9 10 sylancr ⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
12 eqid ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) )
13 1 2 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
14 3 13 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
15 1 5 8 12 14 2 dchrelbas3 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ) ) )
16 3 15 mpbid ⊢ ( 𝜑 → ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ) )
17 16 simprd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
18 17 simp1d ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
19 18 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
20 19 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
21 20 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ∗ ‘ ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
23 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
24 8 12 unitss ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⊆ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
25 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
26 24 25 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
27 23 26 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
29 24 28 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
30 23 29 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
31 27 30 cjmuld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ∗ ‘ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) = ( ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) · ( ∗ ‘ ( 𝑋 ‘ 𝑦 ) ) ) )
32 22 31 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ∗ ‘ ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) ) = ( ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) · ( ∗ ‘ ( 𝑋 ‘ 𝑦 ) ) ) )
33 14 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
34 5 zncrng ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
35 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
36 33 34 35 3syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
38 eqid ⊢ ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) )
39 8 38 ringcl ⊢ ( ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
40 37 26 29 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
41 fvco3 ⊢ ( ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) ) )
42 23 40 41 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) ) )
43 fvco3 ⊢ ( ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) )
44 23 26 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) )
45 fvco3 ⊢ ( ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ 𝑦 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑦 ) ) )
46 23 29 45 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑦 ) ) )
47 44 46 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) ) = ( ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) · ( ∗ ‘ ( 𝑋 ‘ 𝑦 ) ) ) )
48 32 42 47 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) ) )
49 48 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) ) )
50 eqid ⊢ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) )
51 8 50 ringidcl ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
52 36 51 syl ⊢ ( 𝜑 → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
53 fvco3 ⊢ ( ( 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
54 9 52 53 syl2anc ⊢ ( 𝜑 → ( ( ∗ ∘ 𝑋 ) ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
55 17 simp2d ⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 )
56 55 fveq2d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( ∗ ‘ 1 ) )
57 1re ⊢ 1 ∈ ℝ
58 cjre ⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
59 57 58 ax-mp ⊢ ( ∗ ‘ 1 ) = 1
60 56 59 eqtrdi ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = 1 )
61 54 60 eqtrd ⊢ ( 𝜑 → ( ( ∗ ∘ 𝑋 ) ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 )
62 17 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
63 9 43 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) )
64 cj0 ⊢ ( ∗ ‘ 0 ) = 0
65 64 eqcomi ⊢ 0 = ( ∗ ‘ 0 )
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 0 = ( ∗ ‘ 0 ) )
67 63 66 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = 0 ↔ ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) = ( ∗ ‘ 0 ) ) )
68 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
69 0cn ⊢ 0 ∈ ℂ
70 cj11 ⊢ ( ( ( 𝑋 ‘ 𝑥 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) = ( ∗ ‘ 0 ) ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
71 68 69 70 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) = ( ∗ ‘ 0 ) ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
72 67 71 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = 0 ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
73 72 necon3bid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 ↔ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) )
74 73 imbi1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↔ ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
75 74 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
76 62 75 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
77 49 61 76 3jca ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) ) ∧ ( ( ∗ ∘ 𝑋 ) ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
78 1 5 8 12 14 2 dchrelbas3 ⊢ ( 𝜑 → ( ( ∗ ∘ 𝑋 ) ∈ 𝐷 ↔ ( ( ∗ ∘ 𝑋 ) : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ∗ ∘ 𝑋 ) ‘ ( 𝑥 ( .r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) 𝑦 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑦 ) ) ∧ ( ( ∗ ∘ 𝑋 ) ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ) ) )
79 11 77 78 mpbir2and ⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ 𝐷 )
80 1 5 2 6 3 79 dchrmul ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) )
82 81 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) )
83 24 sseli ⊢ ( 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
84 83 63 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) )
85 84 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
86 83 68 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
87 86 absvalsqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ 𝑥 ) ) ↑ 2 ) = ( ( 𝑋 ‘ 𝑥 ) · ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
88 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑋 ∈ 𝐷 )
89 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
90 1 2 88 5 12 89 dchrabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( abs ‘ ( 𝑋 ‘ 𝑥 ) ) = 1 )
91 90 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ 𝑥 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
92 sq1 ⊢ ( 1 ↑ 2 ) = 1
93 91 92 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ 𝑥 ) ) ↑ 2 ) = 1 )
94 85 87 93 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ) = 1 )
95 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑋 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
96 95 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑋 Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
97 11 ffnd ⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ∗ ∘ 𝑋 ) Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
99 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V )
100 83 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
101 fnfvof ⊢ ( ( ( 𝑋 Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( ∗ ∘ 𝑋 ) Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∧ ( ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ) )
102 96 98 99 100 101 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) · ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) ) )
103 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
104 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
105 1 5 103 12 104 89 dchr1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 0g ‘ 𝐺 ) ‘ 𝑥 ) = 1 )
106 94 102 105 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ∘f · ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 0g ‘ 𝐺 ) ‘ 𝑥 ) )
107 82 106 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 0g ‘ 𝐺 ) ‘ 𝑥 ) )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 0g ‘ 𝐺 ) ‘ 𝑥 ) )
109 1 5 2 6 3 79 dchrmulcl ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) ∈ 𝐷 )
110 1 dchrabl ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
111 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
112 14 110 111 3syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
113 2 103 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
114 112 113 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
115 1 5 2 12 109 114 dchreq ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 0g ‘ 𝐺 ) ‘ 𝑥 ) ) )
116 108 115 mpbird ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
117 2 6 103 4 grpinvid1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ∧ ( ∗ ∘ 𝑋 ) ∈ 𝐷 ) → ( ( 𝐼 ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) ) )
118 112 3 79 117 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ∗ ∘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) ) )
119 116 118 mpbird ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) )