Proof of Theorem odeq
Step | Hyp | Ref
| Expression |
1 | | nn0z 12343 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
2 | | odcl.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
3 | | odcl.2 |
. . . . . . . 8
⊢ 𝑂 = (od‘𝐺) |
4 | | odid.3 |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
5 | | odid.4 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
6 | 2, 3, 4, 5 | oddvds 19155 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) |
7 | 1, 6 | syl3an3 1164 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) |
8 | 7 | 3expa 1117 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) |
9 | 8 | ralrimiva 3103 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ ℕ0 ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) |
10 | | breq1 5077 |
. . . . . 6
⊢ (𝑁 = (𝑂‘𝐴) → (𝑁 ∥ 𝑦 ↔ (𝑂‘𝐴) ∥ 𝑦)) |
11 | 10 | bibi1d 344 |
. . . . 5
⊢ (𝑁 = (𝑂‘𝐴) → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |
12 | 11 | ralbidv 3112 |
. . . 4
⊢ (𝑁 = (𝑂‘𝐴) → (∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ ∀𝑦 ∈ ℕ0
((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |
13 | 9, 12 | syl5ibrcom 246 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁 = (𝑂‘𝐴) → ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |
14 | 13 | 3adant3 1131 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘𝐴) → ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |
15 | | simpl3 1192 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∈
ℕ0) |
16 | | simpl2 1191 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝐴 ∈ 𝑋) |
17 | 2, 3 | odcl 19144 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈
ℕ0) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑂‘𝐴) ∈
ℕ0) |
19 | 2, 3, 4, 5 | odid 19146 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 ) |
20 | 16, 19 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → ((𝑂‘𝐴) · 𝐴) = 0 ) |
21 | 17 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑂‘𝐴) ∈
ℕ0) |
22 | | breq2 5078 |
. . . . . . . 8
⊢ (𝑦 = (𝑂‘𝐴) → (𝑁 ∥ 𝑦 ↔ 𝑁 ∥ (𝑂‘𝐴))) |
23 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑦 = (𝑂‘𝐴) → (𝑦 · 𝐴) = ((𝑂‘𝐴) · 𝐴)) |
24 | 23 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑦 = (𝑂‘𝐴) → ((𝑦 · 𝐴) = 0 ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) |
25 | 22, 24 | bibi12d 346 |
. . . . . . 7
⊢ (𝑦 = (𝑂‘𝐴) → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 ))) |
26 | 25 | rspcva 3559 |
. . . . . 6
⊢ (((𝑂‘𝐴) ∈ ℕ0 ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) |
27 | 21, 26 | sylan 580 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) |
28 | 20, 27 | mpbird 256 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∥ (𝑂‘𝐴)) |
29 | | nn0z 12343 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
30 | | iddvds 15979 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) |
31 | 15, 29, 30 | 3syl 18 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∥ 𝑁) |
32 | | breq2 5078 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝑁 ∥ 𝑦 ↔ 𝑁 ∥ 𝑁)) |
33 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (𝑦 · 𝐴) = (𝑁 · 𝐴)) |
34 | 33 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → ((𝑦 · 𝐴) = 0 ↔ (𝑁 · 𝐴) = 0 )) |
35 | 32, 34 | bibi12d 346 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))) |
36 | 35 | rspcva 3559 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) |
37 | 36 | 3ad2antl3 1186 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) |
38 | 31, 37 | mpbid 231 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 · 𝐴) = 0 ) |
39 | 2, 3, 4, 5 | oddvds 19155 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) |
40 | 29, 39 | syl3an3 1164 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) |
41 | 40 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) |
42 | 38, 41 | mpbird 256 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑂‘𝐴) ∥ 𝑁) |
43 | | dvdseq 16023 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ (𝑂‘𝐴) ∈ ℕ0)
∧ (𝑁 ∥ (𝑂‘𝐴) ∧ (𝑂‘𝐴) ∥ 𝑁)) → 𝑁 = (𝑂‘𝐴)) |
44 | 15, 18, 28, 42, 43 | syl22anc 836 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 = (𝑂‘𝐴)) |
45 | 44 | ex 413 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) →
(∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) → 𝑁 = (𝑂‘𝐴))) |
46 | 14, 45 | impbid 211 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘𝐴) ↔ ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |