| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1192 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → 𝐺 ∈ Grp) | 
| 2 |  | odf1o1.x | . . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) | 
| 3 | 2 | subgacs 19179 | . . . . . . 7
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘𝑋)) | 
| 4 |  | acsmre 17695 | . . . . . . 7
⊢
((SubGrp‘𝐺)
∈ (ACS‘𝑋) →
(SubGrp‘𝐺) ∈
(Moore‘𝑋)) | 
| 5 | 1, 3, 4 | 3syl 18 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → (SubGrp‘𝐺) ∈ (Moore‘𝑋)) | 
| 6 |  | simpl2 1193 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ 𝑋) | 
| 7 | 6 | snssd 4809 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → {𝐴} ⊆ 𝑋) | 
| 8 |  | odf1o1.k | . . . . . . 7
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) | 
| 9 | 8 | mrccl 17654 | . . . . . 6
⊢
(((SubGrp‘𝐺)
∈ (Moore‘𝑋)
∧ {𝐴} ⊆ 𝑋) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) | 
| 10 | 5, 7, 9 | syl2anc 584 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) | 
| 11 |  | simpr 484 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) | 
| 12 | 5, 8, 7 | mrcssidd 17668 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → {𝐴} ⊆ (𝐾‘{𝐴})) | 
| 13 |  | snidg 4660 | . . . . . . 7
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴}) | 
| 14 | 6, 13 | syl 17 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ {𝐴}) | 
| 15 | 12, 14 | sseldd 3984 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ (𝐾‘{𝐴})) | 
| 16 |  | odf1o1.t | . . . . . 6
⊢  · =
(.g‘𝐺) | 
| 17 | 16 | subgmulgcl 19157 | . . . . 5
⊢ (((𝐾‘{𝐴}) ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ (𝐾‘{𝐴})) → (𝑥 · 𝐴) ∈ (𝐾‘{𝐴})) | 
| 18 | 10, 11, 15, 17 | syl3anc 1373 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝐴) ∈ (𝐾‘{𝐴})) | 
| 19 | 18 | ex 412 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ → (𝑥 · 𝐴) ∈ (𝐾‘{𝐴}))) | 
| 20 |  | simpl3 1194 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑂‘𝐴) = 0) | 
| 21 | 20 | breq1d 5153 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ 0 ∥ (𝑥 − 𝑦))) | 
| 22 |  | zsubcl 12659 | . . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 − 𝑦) ∈ ℤ) | 
| 23 | 22 | adantl 481 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 − 𝑦) ∈ ℤ) | 
| 24 |  | 0dvds 16314 | . . . . . . 7
⊢ ((𝑥 − 𝑦) ∈ ℤ → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) | 
| 26 | 21, 25 | bitrd 279 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) | 
| 27 |  | simpl1 1192 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐺 ∈ Grp) | 
| 28 |  | simpl2 1193 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ 𝑋) | 
| 29 |  | simprl 771 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℤ) | 
| 30 |  | simprr 773 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℤ) | 
| 31 |  | odf1o1.o | . . . . . . 7
⊢ 𝑂 = (od‘𝐺) | 
| 32 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 33 | 2, 31, 16, 32 | odcong 19567 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ (𝑥 · 𝐴) = (𝑦 · 𝐴))) | 
| 34 | 27, 28, 29, 30, 33 | syl112anc 1376 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ (𝑥 · 𝐴) = (𝑦 · 𝐴))) | 
| 35 |  | zcn 12618 | . . . . . . 7
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) | 
| 36 |  | zcn 12618 | . . . . . . 7
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) | 
| 37 |  | subeq0 11535 | . . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 38 | 35, 36, 37 | syl2an 596 | . . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 39 | 38 | adantl 481 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 40 | 26, 34, 39 | 3bitr3d 309 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 · 𝐴) = (𝑦 · 𝐴) ↔ 𝑥 = 𝑦)) | 
| 41 | 40 | ex 412 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 · 𝐴) = (𝑦 · 𝐴) ↔ 𝑥 = 𝑦))) | 
| 42 | 19, 41 | dom2lem 9032 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1→(𝐾‘{𝐴})) | 
| 43 | 18 | fmpttd 7135 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ⟶(𝐾‘{𝐴})) | 
| 44 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) | 
| 45 | 2, 16, 44, 8 | cycsubg2 19228 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐾‘{𝐴}) = ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))) | 
| 46 | 45 | 3adant3 1133 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝐾‘{𝐴}) = ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))) | 
| 47 | 46 | eqcomd 2743 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) = (𝐾‘{𝐴})) | 
| 48 |  | dffo2 6824 | . . 3
⊢ ((𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–onto→(𝐾‘{𝐴}) ↔ ((𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ⟶(𝐾‘{𝐴}) ∧ ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) = (𝐾‘{𝐴}))) | 
| 49 | 43, 47, 48 | sylanbrc 583 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–onto→(𝐾‘{𝐴})) | 
| 50 |  | df-f1o 6568 | . 2
⊢ ((𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1-onto→(𝐾‘{𝐴}) ↔ ((𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1→(𝐾‘{𝐴}) ∧ (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–onto→(𝐾‘{𝐴}))) | 
| 51 | 42, 49, 50 | sylanbrc 583 | 1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1-onto→(𝐾‘{𝐴})) |