| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → ¬ 𝐵 ∈ Fin) | 
| 2 | 1 | iffalsed 4535 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → if(𝐵 ∈ Fin, (♯‘𝐵), 0) = 0) | 
| 3 |  | ablsimpgfind.1 | . . . . . . 7
⊢ 𝐵 = (Base‘𝐺) | 
| 4 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 5 |  | ablsimpgfind.3 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ SimpGrp) | 
| 6 | 3, 4, 5 | simpgnideld 20120 | . . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = (0g‘𝐺)) | 
| 7 |  | neqne 2947 | . . . . . . 7
⊢ (¬
𝑥 =
(0g‘𝐺)
→ 𝑥 ≠
(0g‘𝐺)) | 
| 8 | 7 | reximi 3083 | . . . . . 6
⊢
(∃𝑥 ∈
𝐵 ¬ 𝑥 = (0g‘𝐺) → ∃𝑥 ∈ 𝐵 𝑥 ≠ (0g‘𝐺)) | 
| 9 | 6, 8 | syl 17 | . . . . 5
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝑥 ≠ (0g‘𝐺)) | 
| 10 |  | eqid 2736 | . . . . . . 7
⊢
(.g‘𝐺) = (.g‘𝐺) | 
| 11 |  | eqid 2736 | . . . . . . 7
⊢
(od‘𝐺) =
(od‘𝐺) | 
| 12 | 5 | simpggrpd 20116 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 13 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → 𝐺 ∈ Grp) | 
| 14 |  | simprl 770 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → 𝑥 ∈ 𝐵) | 
| 15 |  | ablsimpgfind.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ Abel) | 
| 16 | 15 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → 𝐺 ∈ Abel) | 
| 17 | 5 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → 𝐺 ∈ SimpGrp) | 
| 18 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) | 
| 19 |  | simplrr 777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → 𝑥 ≠ (0g‘𝐺)) | 
| 20 | 19 | neneqd 2944 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → ¬ 𝑥 = (0g‘𝐺)) | 
| 21 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) | 
| 22 | 3, 4, 10, 16, 17, 18, 20, 21 | ablsimpg1gend 20126 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) | 
| 23 | 22 | ex 412 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → (𝑦 ∈ 𝐵 → ∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥))) | 
| 24 |  | simprr 772 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → 𝑦 = (𝑛(.g‘𝐺)𝑥)) | 
| 25 | 12 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → 𝐺 ∈ Grp) | 
| 26 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → 𝑛 ∈ ℤ) | 
| 27 | 14 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → 𝑥 ∈ 𝐵) | 
| 28 | 3, 10, 25, 26, 27 | mulgcld 19115 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → (𝑛(.g‘𝐺)𝑥) ∈ 𝐵) | 
| 29 | 24, 28 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) ∧ (𝑛 ∈ ℤ ∧ 𝑦 = (𝑛(.g‘𝐺)𝑥))) → 𝑦 ∈ 𝐵) | 
| 30 | 29 | rexlimdvaa 3155 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → (∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) → 𝑦 ∈ 𝐵)) | 
| 31 | 23, 30 | impbid 212 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → (𝑦 ∈ 𝐵 ↔ ∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥))) | 
| 32 | 31 | eqabdv 2874 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → 𝐵 = {𝑦 ∣ ∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)}) | 
| 33 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) | 
| 34 | 33 | rnmpt 5967 | . . . . . . . 8
⊢ ran
(𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)𝑥)) = {𝑦 ∣ ∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)} | 
| 35 | 32, 34 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → 𝐵 = ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥))) | 
| 36 | 3, 10, 11, 13, 14, 35 | cycsubggenodd 20130 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → ((od‘𝐺)‘𝑥) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) | 
| 37 | 3, 4, 10, 11, 15, 5 | ablsimpgfindlem2 20129 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2(.g‘𝐺)𝑥) = (0g‘𝐺)) → ((od‘𝐺)‘𝑥) ≠ 0) | 
| 38 | 3, 4, 10, 11, 15, 5 | ablsimpgfindlem1 20128 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2(.g‘𝐺)𝑥) ≠ (0g‘𝐺)) → ((od‘𝐺)‘𝑥) ≠ 0) | 
| 39 | 37, 38 | pm2.61dane 3028 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ≠ 0) | 
| 40 | 39 | adantrr 717 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → ((od‘𝐺)‘𝑥) ≠ 0) | 
| 41 | 36, 40 | eqnetrrd 3008 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝐺))) → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ≠ 0) | 
| 42 | 9, 41 | rexlimddv 3160 | . . . 4
⊢ (𝜑 → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ≠ 0) | 
| 43 | 42 | adantr 480 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ≠ 0) | 
| 44 | 2, 43 | pm2.21ddne 3025 | . 2
⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → ⊥) | 
| 45 | 44 | efald 1560 | 1
⊢ (𝜑 → 𝐵 ∈ Fin) |