| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dchrabs.g | . . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) | 
| 2 |  | eqid 2736 | . . . . . . . 8
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) | 
| 3 |  | dchrabs.d | . . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) | 
| 4 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 5 |  | dchrabs.x | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) | 
| 6 |  | cjf 15144 | . . . . . . . . . 10
⊢
∗:ℂ⟶ℂ | 
| 7 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) | 
| 8 | 1, 2, 3, 7, 5 | dchrf 27287 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 9 |  | fco 6759 | . . . . . . . . . 10
⊢
((∗:ℂ⟶ℂ ∧ 𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) → (∗
∘ 𝑋):(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 10 | 6, 8, 9 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (∗ ∘ 𝑋):(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 11 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) | 
| 12 | 1, 3 | dchrrcl 27285 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) | 
| 13 | 5, 12 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 14 | 1, 2, 7, 11, 13, 3 | dchrelbas3 27283 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧
(∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘(ℤ/nℤ‘𝑁))) = 1 ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))((𝑋‘𝑥)
≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))))) | 
| 15 | 5, 14 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧
(∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘(ℤ/nℤ‘𝑁))) = 1 ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))((𝑋‘𝑥)
≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))))) | 
| 16 | 15 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘(ℤ/nℤ‘𝑁))) = 1 ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))((𝑋‘𝑥)
≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 17 | 16 | simp1d 1142 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 18 | 17 | r19.21bi 3250 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 19 | 18 | r19.21bi 3250 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → (𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 20 | 19 | anasss 466 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) | 
| 21 | 20 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (∗‘(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦))) = (∗‘((𝑋‘𝑥) · (𝑋‘𝑦)))) | 
| 22 | 8 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → 𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 23 | 7, 11 | unitss 20377 | . . . . . . . . . . . . . . . 16
⊢
(Unit‘(ℤ/nℤ‘𝑁)) ⊆
(Base‘(ℤ/nℤ‘𝑁)) | 
| 24 |  | simprl 770 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) | 
| 25 | 23, 24 | sselid 3980 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 26 | 22, 25 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (𝑋‘𝑥) ∈ ℂ) | 
| 27 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))) | 
| 28 | 23, 27 | sselid 3980 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → 𝑦 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 29 | 22, 28 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (𝑋‘𝑦) ∈ ℂ) | 
| 30 | 26, 29 | cjmuld 15261 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (∗‘((𝑋‘𝑥) · (𝑋‘𝑦))) = ((∗‘(𝑋‘𝑥)) · (∗‘(𝑋‘𝑦)))) | 
| 31 | 21, 30 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (∗‘(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦))) = ((∗‘(𝑋‘𝑥)) · (∗‘(𝑋‘𝑦)))) | 
| 32 | 13 | nnnn0d 12589 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 33 | 2 | zncrng 21564 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) | 
| 34 |  | crngring 20243 | . . . . . . . . . . . . . . . 16
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 35 | 32, 33, 34 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(.r‘(ℤ/nℤ‘𝑁)) =
(.r‘(ℤ/nℤ‘𝑁)) | 
| 38 | 7, 37 | ringcl 20248 | . . . . . . . . . . . . . 14
⊢
(((ℤ/nℤ‘𝑁) ∈ Ring ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦) ∈ (Base‘(ℤ/nℤ‘𝑁))) | 
| 39 | 36, 25, 28, 38 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦) ∈ (Base‘(ℤ/nℤ‘𝑁))) | 
| 40 |  | fvco3 7007 | . . . . . . . . . . . . 13
⊢ ((𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ (𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦) ∈ (Base‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (∗‘(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)))) | 
| 41 | 22, 39, 40 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → ((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (∗‘(𝑋‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)))) | 
| 42 |  | fvco3 7007 | . . . . . . . . . . . . . 14
⊢ ((𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) | 
| 43 | 22, 25, 42 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) | 
| 44 |  | fvco3 7007 | . . . . . . . . . . . . . 14
⊢ ((𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑦 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘𝑦) = (∗‘(𝑋‘𝑦))) | 
| 45 | 22, 28, 44 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → ((∗ ∘ 𝑋)‘𝑦) = (∗‘(𝑋‘𝑦))) | 
| 46 | 43, 45 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → (((∗ ∘ 𝑋)‘𝑥) · ((∗ ∘ 𝑋)‘𝑦)) = ((∗‘(𝑋‘𝑥)) · (∗‘(𝑋‘𝑦)))) | 
| 47 | 31, 41, 46 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ 𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) → ((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (((∗ ∘ 𝑋)‘𝑥) · ((∗ ∘ 𝑋)‘𝑦))) | 
| 48 | 47 | ralrimivva 3201 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (((∗ ∘ 𝑋)‘𝑥) · ((∗ ∘ 𝑋)‘𝑦))) | 
| 49 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) | 
| 50 | 7, 49 | ringidcl 20263 | . . . . . . . . . . . . 13
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 51 | 35, 50 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 →
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 52 |  | fvco3 7007 | . . . . . . . . . . . 12
⊢ ((𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘(1r‘(ℤ/nℤ‘𝑁))) = (∗‘(𝑋‘(1r‘(ℤ/nℤ‘𝑁))))) | 
| 53 | 8, 51, 52 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((∗ ∘ 𝑋)‘(1r‘(ℤ/nℤ‘𝑁))) = (∗‘(𝑋‘(1r‘(ℤ/nℤ‘𝑁))))) | 
| 54 | 16 | simp2d 1143 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋‘(1r‘(ℤ/nℤ‘𝑁))) = 1) | 
| 55 | 54 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(𝑋‘(1r‘(ℤ/nℤ‘𝑁)))) = (∗‘1)) | 
| 56 |  | 1re 11262 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ | 
| 57 |  | cjre 15179 | . . . . . . . . . . . . 13
⊢ (1 ∈
ℝ → (∗‘1) = 1) | 
| 58 | 56, 57 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(∗‘1) = 1 | 
| 59 | 55, 58 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝜑 → (∗‘(𝑋‘(1r‘(ℤ/nℤ‘𝑁)))) = 1) | 
| 60 | 53, 59 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → ((∗ ∘ 𝑋)‘(1r‘(ℤ/nℤ‘𝑁))) = 1) | 
| 61 | 16 | simp3d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))((𝑋‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 62 | 8, 42 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) | 
| 63 |  | cj0 15198 | . . . . . . . . . . . . . . . . . 18
⊢
(∗‘0) = 0 | 
| 64 | 63 | eqcomi 2745 | . . . . . . . . . . . . . . . . 17
⊢ 0 =
(∗‘0) | 
| 65 | 64 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → 0 =
(∗‘0)) | 
| 66 | 62, 65 | eqeq12d 2752 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (((∗ ∘ 𝑋)‘𝑥) = 0 ↔ (∗‘(𝑋‘𝑥)) = (∗‘0))) | 
| 67 | 8 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑋‘𝑥) ∈ ℂ) | 
| 68 |  | 0cn 11254 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℂ | 
| 69 |  | cj11 15202 | . . . . . . . . . . . . . . . 16
⊢ (((𝑋‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ)
→ ((∗‘(𝑋‘𝑥)) = (∗‘0) ↔ (𝑋‘𝑥) = 0)) | 
| 70 | 67, 68, 69 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((∗‘(𝑋‘𝑥)) = (∗‘0) ↔ (𝑋‘𝑥) = 0)) | 
| 71 | 66, 70 | bitrd 279 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (((∗ ∘ 𝑋)‘𝑥) = 0 ↔ (𝑋‘𝑥) = 0)) | 
| 72 | 71 | necon3bid 2984 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (((∗ ∘ 𝑋)‘𝑥) ≠ 0 ↔ (𝑋‘𝑥) ≠ 0)) | 
| 73 | 72 | imbi1d 341 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((((∗ ∘ 𝑋)‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) ↔ ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 74 | 73 | ralbidva 3175 | . . . . . . . . . . 11
⊢ (𝜑 → (∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(((∗ ∘ 𝑋)‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) ↔ ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))((𝑋‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 75 | 61, 74 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(((∗ ∘ 𝑋)‘𝑥) ≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 76 | 48, 60, 75 | 3jca 1128 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (((∗ ∘ 𝑋)‘𝑥) · ((∗ ∘ 𝑋)‘𝑦)) ∧ ((∗ ∘ 𝑋)‘(1r‘(ℤ/nℤ‘𝑁))) = 1 ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))(((∗ ∘ 𝑋)‘𝑥)
≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 77 | 1, 2, 7, 11, 13, 3 | dchrelbas3 27283 | . . . . . . . . 9
⊢ (𝜑 → ((∗ ∘ 𝑋) ∈ 𝐷 ↔ ((∗ ∘ 𝑋):(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ (∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))∀𝑦 ∈
(Unit‘(ℤ/nℤ‘𝑁))((∗ ∘ 𝑋)‘(𝑥(.r‘(ℤ/nℤ‘𝑁))𝑦)) = (((∗ ∘ 𝑋)‘𝑥) · ((∗ ∘ 𝑋)‘𝑦)) ∧ ((∗ ∘ 𝑋)‘(1r‘(ℤ/nℤ‘𝑁))) = 1 ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))(((∗ ∘ 𝑋)‘𝑥)
≠ 0 → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))))))) | 
| 78 | 10, 76, 77 | mpbir2and 713 | . . . . . . . 8
⊢ (𝜑 → (∗ ∘ 𝑋) ∈ 𝐷) | 
| 79 | 1, 2, 3, 4, 5, 78 | dchrmul 27293 | . . . . . . 7
⊢ (𝜑 → (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (𝑋 ∘f · (∗
∘ 𝑋))) | 
| 80 | 79 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (𝑋 ∘f · (∗
∘ 𝑋))) | 
| 81 | 80 | fveq1d 6907 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋(+g‘𝐺)(∗ ∘ 𝑋))‘𝑥) = ((𝑋 ∘f · (∗
∘ 𝑋))‘𝑥)) | 
| 82 | 23 | sseli 3978 | . . . . . . . . 9
⊢ (𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 83 | 82, 62 | sylan2 593 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) | 
| 84 | 83 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋‘𝑥) · ((∗ ∘ 𝑋)‘𝑥)) = ((𝑋‘𝑥) · (∗‘(𝑋‘𝑥)))) | 
| 85 | 82, 67 | sylan2 593 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → (𝑋‘𝑥) ∈ ℂ) | 
| 86 | 85 | absvalsqd 15482 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((abs‘(𝑋‘𝑥))↑2) = ((𝑋‘𝑥) · (∗‘(𝑋‘𝑥)))) | 
| 87 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑋 ∈ 𝐷) | 
| 88 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) | 
| 89 | 1, 3, 87, 2, 11, 88 | dchrabs 27305 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → (abs‘(𝑋‘𝑥)) = 1) | 
| 90 | 89 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((abs‘(𝑋‘𝑥))↑2) = (1↑2)) | 
| 91 |  | sq1 14235 | . . . . . . . 8
⊢
(1↑2) = 1 | 
| 92 | 90, 91 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((abs‘(𝑋‘𝑥))↑2) = 1) | 
| 93 | 84, 86, 92 | 3eqtr2d 2782 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋‘𝑥) · ((∗ ∘ 𝑋)‘𝑥)) = 1) | 
| 94 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑋:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 95 | 94 | ffnd 6736 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑋 Fn
(Base‘(ℤ/nℤ‘𝑁))) | 
| 96 | 10 | ffnd 6736 | . . . . . . . 8
⊢ (𝜑 → (∗ ∘ 𝑋) Fn
(Base‘(ℤ/nℤ‘𝑁))) | 
| 97 | 96 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → (∗ ∘ 𝑋) Fn
(Base‘(ℤ/nℤ‘𝑁))) | 
| 98 |  | fvexd 6920 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) | 
| 99 | 82 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 100 |  | fnfvof 7715 | . . . . . . 7
⊢ (((𝑋 Fn
(Base‘(ℤ/nℤ‘𝑁)) ∧ (∗ ∘ 𝑋) Fn
(Base‘(ℤ/nℤ‘𝑁))) ∧
((Base‘(ℤ/nℤ‘𝑁)) ∈ V ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)))) → ((𝑋 ∘f · (∗
∘ 𝑋))‘𝑥) = ((𝑋‘𝑥) · ((∗ ∘ 𝑋)‘𝑥))) | 
| 101 | 95, 97, 98, 99, 100 | syl22anc 838 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋 ∘f · (∗
∘ 𝑋))‘𝑥) = ((𝑋‘𝑥) · ((∗ ∘ 𝑋)‘𝑥))) | 
| 102 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 103 | 13 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → 𝑁 ∈ ℕ) | 
| 104 | 1, 2, 102, 11, 103, 88 | dchr1 27302 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((0g‘𝐺)‘𝑥) = 1) | 
| 105 | 93, 101, 104 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋 ∘f · (∗
∘ 𝑋))‘𝑥) = ((0g‘𝐺)‘𝑥)) | 
| 106 | 81, 105 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((𝑋(+g‘𝐺)(∗ ∘ 𝑋))‘𝑥) = ((0g‘𝐺)‘𝑥)) | 
| 107 | 106 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))((𝑋(+g‘𝐺)(∗ ∘ 𝑋))‘𝑥) = ((0g‘𝐺)‘𝑥)) | 
| 108 | 1, 2, 3, 4, 5, 78 | dchrmulcl 27294 | . . . 4
⊢ (𝜑 → (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) ∈ 𝐷) | 
| 109 | 1 | dchrabl 27299 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) | 
| 110 |  | ablgrp 19804 | . . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | 
| 111 | 13, 109, 110 | 3syl 18 | . . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 112 | 3, 102 | grpidcl 18984 | . . . . 5
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐷) | 
| 113 | 111, 112 | syl 17 | . . . 4
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐷) | 
| 114 | 1, 2, 3, 11, 108, 113 | dchreq 27303 | . . 3
⊢ (𝜑 → ((𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (0g‘𝐺) ↔ ∀𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))((𝑋(+g‘𝐺)(∗ ∘ 𝑋))‘𝑥) = ((0g‘𝐺)‘𝑥))) | 
| 115 | 107, 114 | mpbird 257 | . 2
⊢ (𝜑 → (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (0g‘𝐺)) | 
| 116 |  | dchrinv.i | . . . 4
⊢ 𝐼 = (invg‘𝐺) | 
| 117 | 3, 4, 102, 116 | grpinvid1 19010 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ∧ (∗ ∘ 𝑋) ∈ 𝐷) → ((𝐼‘𝑋) = (∗ ∘ 𝑋) ↔ (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (0g‘𝐺))) | 
| 118 | 111, 5, 78, 117 | syl3anc 1372 | . 2
⊢ (𝜑 → ((𝐼‘𝑋) = (∗ ∘ 𝑋) ↔ (𝑋(+g‘𝐺)(∗ ∘ 𝑋)) = (0g‘𝐺))) | 
| 119 | 115, 118 | mpbird 257 | 1
⊢ (𝜑 → (𝐼‘𝑋) = (∗ ∘ 𝑋)) |