Step | Hyp | Ref
| Expression |
1 | | odf1.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
2 | | odf1.3 |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
3 | 1, 2 | mulgcl 17382 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
4 | 3 | 3expa 1257 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ) ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
5 | 4 | an32s 842 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝐴) ∈ 𝑋) |
6 | | odf1.4 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) |
7 | 5, 6 | fmptd 6292 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → 𝐹:ℤ⟶𝑋) |
8 | 7 | adantr 480 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) → 𝐹:ℤ⟶𝑋) |
9 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐴) = (𝑦 · 𝐴)) |
10 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑥 · 𝐴) ∈ V |
11 | 9, 6, 10 | fvmpt3i 6196 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ → (𝐹‘𝑦) = (𝑦 · 𝐴)) |
12 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 · 𝐴) = (𝑧 · 𝐴)) |
13 | 12, 6, 10 | fvmpt3i 6196 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤ → (𝐹‘𝑧) = (𝑧 · 𝐴)) |
14 | 11, 13 | eqeqan12d 2626 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝑦 · 𝐴) = (𝑧 · 𝐴))) |
15 | 14 | adantl 481 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝑦 · 𝐴) = (𝑧 · 𝐴))) |
16 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (𝑂‘𝐴) = 0) |
17 | 16 | breq1d 4593 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑦 − 𝑧) ↔ 0 ∥ (𝑦 − 𝑧))) |
18 | | odf1.2 |
. . . . . . . . . 10
⊢ 𝑂 = (od‘𝐺) |
19 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
20 | 1, 18, 2, 19 | odcong 17791 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑦 − 𝑧) ↔ (𝑦 · 𝐴) = (𝑧 · 𝐴))) |
21 | 20 | 3expa 1257 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑦 − 𝑧) ↔ (𝑦 · 𝐴) = (𝑧 · 𝐴))) |
22 | 21 | adantlr 747 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑦 − 𝑧) ↔ (𝑦 · 𝐴) = (𝑧 · 𝐴))) |
23 | | zsubcl 11296 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑦 − 𝑧) ∈ ℤ) |
24 | 23 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (𝑦 − 𝑧) ∈ ℤ) |
25 | | 0dvds 14840 |
. . . . . . . 8
⊢ ((𝑦 − 𝑧) ∈ ℤ → (0 ∥ (𝑦 − 𝑧) ↔ (𝑦 − 𝑧) = 0)) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (0 ∥ (𝑦 − 𝑧) ↔ (𝑦 − 𝑧) = 0)) |
27 | 17, 22, 26 | 3bitr3d 297 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) = (𝑧 · 𝐴) ↔ (𝑦 − 𝑧) = 0)) |
28 | | zcn 11259 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
29 | | zcn 11259 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) |
30 | | subeq0 10186 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑦 − 𝑧) = 0 ↔ 𝑦 = 𝑧)) |
31 | 28, 29, 30 | syl2an 493 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 − 𝑧) = 0 ↔ 𝑦 = 𝑧)) |
32 | 31 | adantl 481 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝑦 − 𝑧) = 0 ↔ 𝑦 = 𝑧)) |
33 | 15, 27, 32 | 3bitrd 293 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) |
34 | 33 | biimpd 218 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) ∧ (𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
35 | 34 | ralrimivva 2954 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) → ∀𝑦 ∈ ℤ ∀𝑧 ∈ ℤ ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
36 | | dff13 6416 |
. . 3
⊢ (𝐹:ℤ–1-1→𝑋 ↔ (𝐹:ℤ⟶𝑋 ∧ ∀𝑦 ∈ ℤ ∀𝑧 ∈ ℤ ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
37 | 8, 35, 36 | sylanbrc 695 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) → 𝐹:ℤ–1-1→𝑋) |
38 | 1, 18, 2, 19 | odid 17780 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = (0g‘𝐺)) |
39 | 1, 19, 2 | mulg0 17369 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → (0 · 𝐴) = (0g‘𝐺)) |
40 | 38, 39 | eqtr4d 2647 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = (0 · 𝐴)) |
41 | 40 | ad2antlr 759 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → ((𝑂‘𝐴) · 𝐴) = (0 · 𝐴)) |
42 | 1, 18 | odcl 17778 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈
ℕ0) |
43 | 42 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝑂‘𝐴) ∈
ℕ0) |
44 | 43 | nn0zd 11356 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝑂‘𝐴) ∈ ℤ) |
45 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (𝑂‘𝐴) → (𝑥 · 𝐴) = ((𝑂‘𝐴) · 𝐴)) |
46 | 45, 6, 10 | fvmpt3i 6196 |
. . . . 5
⊢ ((𝑂‘𝐴) ∈ ℤ → (𝐹‘(𝑂‘𝐴)) = ((𝑂‘𝐴) · 𝐴)) |
47 | 44, 46 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝐹‘(𝑂‘𝐴)) = ((𝑂‘𝐴) · 𝐴)) |
48 | | 0zd 11266 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → 0 ∈ ℤ) |
49 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 · 𝐴) = (0 · 𝐴)) |
50 | 49, 6, 10 | fvmpt3i 6196 |
. . . . 5
⊢ (0 ∈
ℤ → (𝐹‘0)
= (0 · 𝐴)) |
51 | 48, 50 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝐹‘0) = (0 · 𝐴)) |
52 | 41, 47, 51 | 3eqtr4d 2654 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝐹‘(𝑂‘𝐴)) = (𝐹‘0)) |
53 | | simpr 476 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → 𝐹:ℤ–1-1→𝑋) |
54 | | f1fveq 6420 |
. . . 4
⊢ ((𝐹:ℤ–1-1→𝑋 ∧ ((𝑂‘𝐴) ∈ ℤ ∧ 0 ∈ ℤ))
→ ((𝐹‘(𝑂‘𝐴)) = (𝐹‘0) ↔ (𝑂‘𝐴) = 0)) |
55 | 53, 44, 48, 54 | syl12anc 1316 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → ((𝐹‘(𝑂‘𝐴)) = (𝐹‘0) ↔ (𝑂‘𝐴) = 0)) |
56 | 52, 55 | mpbid 221 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:ℤ–1-1→𝑋) → (𝑂‘𝐴) = 0) |
57 | 37, 56 | impbida 873 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝑂‘𝐴) = 0 ↔ 𝐹:ℤ–1-1→𝑋)) |