Proof of Theorem odeq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0z 12638 | . . . . . . 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 19565 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) | 
| 7 | 1, 6 | syl3an3 1166 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) | 
| 8 | 7 | 3expa 1119 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) | 
| 9 | 8 | ralrimiva 3146 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ ℕ0 ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) | 
| 10 |  | breq1 5146 | . . . . . 6
⊢ (𝑁 = (𝑂‘𝐴) → (𝑁 ∥ 𝑦 ↔ (𝑂‘𝐴) ∥ 𝑦)) | 
| 11 | 10 | bibi1d 343 | . . . . 5
⊢ (𝑁 = (𝑂‘𝐴) → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ ((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) | 
| 12 | 11 | ralbidv 3178 | . . . 4
⊢ (𝑁 = (𝑂‘𝐴) → (∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ ∀𝑦 ∈ ℕ0
((𝑂‘𝐴) ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) | 
| 13 | 9, 12 | syl5ibrcom 247 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁 = (𝑂‘𝐴) → ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) | 
| 14 | 13 | 3adant3 1133 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘𝐴) → ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) | 
| 15 |  | simpl3 1194 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∈
ℕ0) | 
| 16 |  | simpl2 1193 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝐴 ∈ 𝑋) | 
| 17 | 2, 3 | odcl 19554 | . . . . 5
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈
ℕ0) | 
| 18 | 16, 17 | syl 17 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑂‘𝐴) ∈
ℕ0) | 
| 19 | 2, 3, 4, 5 | odid 19556 | . . . . . 6
⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 ) | 
| 20 | 16, 19 | syl 17 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → ((𝑂‘𝐴) · 𝐴) = 0 ) | 
| 21 | 17 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑂‘𝐴) ∈
ℕ0) | 
| 22 |  | breq2 5147 | . . . . . . . 8
⊢ (𝑦 = (𝑂‘𝐴) → (𝑁 ∥ 𝑦 ↔ 𝑁 ∥ (𝑂‘𝐴))) | 
| 23 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑦 = (𝑂‘𝐴) → (𝑦 · 𝐴) = ((𝑂‘𝐴) · 𝐴)) | 
| 24 | 23 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑦 = (𝑂‘𝐴) → ((𝑦 · 𝐴) = 0 ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) | 
| 25 | 22, 24 | bibi12d 345 | . . . . . . 7
⊢ (𝑦 = (𝑂‘𝐴) → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 ))) | 
| 26 | 25 | rspcva 3620 | . . . . . 6
⊢ (((𝑂‘𝐴) ∈ ℕ0 ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) | 
| 27 | 21, 26 | sylan 580 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) · 𝐴) = 0 )) | 
| 28 | 20, 27 | mpbird 257 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∥ (𝑂‘𝐴)) | 
| 29 |  | nn0z 12638 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 30 |  | iddvds 16307 | . . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) | 
| 31 | 15, 29, 30 | 3syl 18 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 ∥ 𝑁) | 
| 32 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝑁 ∥ 𝑦 ↔ 𝑁 ∥ 𝑁)) | 
| 33 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (𝑦 · 𝐴) = (𝑁 · 𝐴)) | 
| 34 | 33 | eqeq1d 2739 | . . . . . . . . 9
⊢ (𝑦 = 𝑁 → ((𝑦 · 𝐴) = 0 ↔ (𝑁 · 𝐴) = 0 )) | 
| 35 | 32, 34 | bibi12d 345 | . . . . . . . 8
⊢ (𝑦 = 𝑁 → ((𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) ↔ (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))) | 
| 36 | 35 | rspcva 3620 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) | 
| 37 | 36 | 3ad2antl3 1188 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) | 
| 38 | 31, 37 | mpbid 232 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑁 · 𝐴) = 0 ) | 
| 39 | 2, 3, 4, 5 | oddvds 19565 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) | 
| 40 | 29, 39 | syl3an3 1166 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) | 
| 41 | 40 | adantr 480 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 )) | 
| 42 | 38, 41 | mpbird 257 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → (𝑂‘𝐴) ∥ 𝑁) | 
| 43 |  | dvdseq 16351 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ (𝑂‘𝐴) ∈ ℕ0)
∧ (𝑁 ∥ (𝑂‘𝐴) ∧ (𝑂‘𝐴) ∥ 𝑁)) → 𝑁 = (𝑂‘𝐴)) | 
| 44 | 15, 18, 28, 42, 43 | syl22anc 839 | . . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )) → 𝑁 = (𝑂‘𝐴)) | 
| 45 | 44 | ex 412 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) →
(∀𝑦 ∈
ℕ0 (𝑁
∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ) → 𝑁 = (𝑂‘𝐴))) | 
| 46 | 14, 45 | impbid 212 | 1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘𝐴) ↔ ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 ))) |