| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → (𝑛 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥)) |
| 2 | 1 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → ((𝑛 ↑ 𝑥) = (0g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺))) |
| 3 | 2 | rabbidv 3444 |
. . . . . 6
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 4 | 3 | fveq2d 6910 |
. . . . 5
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 5 | | id 22 |
. . . . 5
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → 𝑛 = ((od‘𝐺)‘𝐴)) |
| 6 | 4, 5 | breq12d 5156 |
. . . 4
⊢ (𝑛 = ((od‘𝐺)‘𝐴) → ((♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ≤ ((od‘𝐺)‘𝐴))) |
| 7 | | unitscyglem1.5 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) |
| 8 | | unitscyglem1.3 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 9 | | unitscyglem1.4 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 10 | | unitscyglem1.6 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 11 | | unitscyglem1.1 |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 12 | | eqid 2737 |
. . . . . 6
⊢
(od‘𝐺) =
(od‘𝐺) |
| 13 | 11, 12 | odcl2 19583 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵) → ((od‘𝐺)‘𝐴) ∈ ℕ) |
| 14 | 8, 9, 10, 13 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈ ℕ) |
| 15 | 6, 7, 14 | rspcdva 3623 |
. . 3
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ≤ ((od‘𝐺)‘𝐴)) |
| 16 | | unitscyglem1.2 |
. . . . . . 7
⊢ ↑ =
(.g‘𝐺) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) = (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) |
| 18 | 11, 12, 16, 17 | dfod2 19582 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → ((od‘𝐺)‘𝐴) = if(ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ∈ Fin, (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))), 0)) |
| 19 | 8, 10, 18 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = if(ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ∈ Fin, (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))), 0)) |
| 20 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → 𝐺 ∈ Grp) |
| 21 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) |
| 22 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → 𝐴 ∈ 𝐵) |
| 23 | 11, 16, 20, 21, 22 | mulgcld 19114 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → (𝑖 ↑ 𝐴) ∈ 𝐵) |
| 24 | 23 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)):ℤ⟶𝐵) |
| 25 | | frn 6743 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)):ℤ⟶𝐵 → ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ⊆ 𝐵) |
| 26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ⊆ 𝐵) |
| 27 | 9, 26 | ssfid 9301 |
. . . . . 6
⊢ (𝜑 → ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ∈ Fin) |
| 28 | 27 | iftrued 4533 |
. . . . 5
⊢ (𝜑 → if(ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ∈ Fin, (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))), 0) = (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)))) |
| 29 | 19, 28 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)))) |
| 30 | | eqid 2737 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} |
| 31 | | fvexd 6921 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐺) ∈ V) |
| 32 | 11, 31 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
| 33 | 30, 32 | rabexd 5340 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ∈ V) |
| 34 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℤ) → (𝑖 ↑ 𝐴) ∈ V) |
| 35 | 34 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)):ℤ⟶V) |
| 36 | 35 | ffnd 6737 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) Fn ℤ) |
| 37 | | fvelrnb 6969 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) Fn ℤ → (𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ↔ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦)) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ↔ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦)) |
| 39 | 38 | biimpa 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) → ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) |
| 40 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦 → ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) |
| 41 | 40 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦 → 𝑦 = ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤)) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) ∧ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) → 𝑦 = ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤)) |
| 43 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) → 𝜑) |
| 44 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ ℤ) |
| 45 | 43, 44 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) → (𝜑 ∧ 𝑤 ∈ ℤ)) |
| 46 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) = (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ ℤ) ∧ 𝑖 = 𝑤) → 𝑖 = 𝑤) |
| 48 | 47 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ ℤ) ∧ 𝑖 = 𝑤) → (𝑖 ↑ 𝐴) = (𝑤 ↑ 𝐴)) |
| 49 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → 𝑤 ∈ ℤ) |
| 50 | | ovexd 7466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑ 𝐴) ∈ V) |
| 51 | 46, 48, 49, 50 | fvmptd 7023 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = (𝑤 ↑ 𝐴)) |
| 52 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑤 ↑ 𝐴) → (((od‘𝐺)‘𝐴) ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ (𝑤 ↑ 𝐴))) |
| 53 | 52 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑤 ↑ 𝐴) → ((((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ (𝑤 ↑ 𝐴)) = (0g‘𝐺))) |
| 54 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → 𝐺 ∈ Grp) |
| 55 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → 𝐴 ∈ 𝐵) |
| 56 | 11, 16, 54, 49, 55 | mulgcld 19114 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑ 𝐴) ∈ 𝐵) |
| 57 | 14 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈ ℤ) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((od‘𝐺)‘𝐴) ∈ ℤ) |
| 59 | 49, 58, 55 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ∈ ℤ ∧ ((od‘𝐺)‘𝐴) ∈ ℤ ∧ 𝐴 ∈ 𝐵)) |
| 60 | 11, 16 | mulgass 19129 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ (𝑤 ∈ ℤ ∧
((od‘𝐺)‘𝐴) ∈ ℤ ∧ 𝐴 ∈ 𝐵)) → ((𝑤 · ((od‘𝐺)‘𝐴)) ↑ 𝐴) = (𝑤 ↑ (((od‘𝐺)‘𝐴) ↑ 𝐴))) |
| 61 | 54, 59, 60 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((𝑤 · ((od‘𝐺)‘𝐴)) ↑ 𝐴) = (𝑤 ↑ (((od‘𝐺)‘𝐴) ↑ 𝐴))) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 63 | 11, 12, 16, 62 | odid 19556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ 𝐵 → (((od‘𝐺)‘𝐴) ↑ 𝐴) = (0g‘𝐺)) |
| 64 | 55, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (((od‘𝐺)‘𝐴) ↑ 𝐴) = (0g‘𝐺)) |
| 65 | 64 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑ (((od‘𝐺)‘𝐴) ↑ 𝐴)) = (𝑤 ↑
(0g‘𝐺))) |
| 66 | 11, 16, 62 | mulgz 19120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ ℤ) → (𝑤 ↑
(0g‘𝐺)) =
(0g‘𝐺)) |
| 67 | 8, 66 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑
(0g‘𝐺)) =
(0g‘𝐺)) |
| 68 | 65, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑ (((od‘𝐺)‘𝐴) ↑ 𝐴)) = (0g‘𝐺)) |
| 69 | 61, 68 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) →
(0g‘𝐺) =
((𝑤 ·
((od‘𝐺)‘𝐴)) ↑ 𝐴)) |
| 70 | 59 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((od‘𝐺)‘𝐴) ∈ ℤ) |
| 71 | 70, 49, 55 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (((od‘𝐺)‘𝐴) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝐴 ∈ 𝐵)) |
| 72 | 11, 16 | mulgassr 19130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧
(((od‘𝐺)‘𝐴) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝐴 ∈ 𝐵)) → ((𝑤 · ((od‘𝐺)‘𝐴)) ↑ 𝐴) = (((od‘𝐺)‘𝐴) ↑ (𝑤 ↑ 𝐴))) |
| 73 | 54, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((𝑤 · ((od‘𝐺)‘𝐴)) ↑ 𝐴) = (((od‘𝐺)‘𝐴) ↑ (𝑤 ↑ 𝐴))) |
| 74 | 69, 73 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (((od‘𝐺)‘𝐴) ↑ (𝑤 ↑ 𝐴)) = (0g‘𝐺)) |
| 75 | 53, 56, 74 | elrabd 3694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → (𝑤 ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 76 | 51, 75 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ℤ) → ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 77 | 45, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) → ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 78 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) ∧ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) → ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 79 | 42, 78 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) ∧ 𝑤 ∈ ℤ) ∧ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 80 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 |
| 81 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦 |
| 82 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 ↔ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦)) |
| 83 | 80, 81, 82 | cbvrexw 3307 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
ℤ ((𝑖 ∈ ℤ
↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 ↔ ∃𝑤 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) |
| 84 | 83 | biimpi 216 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
ℤ ((𝑖 ∈ ℤ
↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 → ∃𝑤 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) |
| 85 | 84 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) → ∃𝑤 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑤) = 𝑦) |
| 86 | 79, 85 | r19.29a 3162 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 87 | 86 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 88 | 87 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) → (∃𝑧 ∈ ℤ ((𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))‘𝑧) = 𝑦 → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 89 | 39, 88 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 90 | 89 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 91 | 90 | ssrdv 3989 |
. . . . 5
⊢ (𝜑 → ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ⊆ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) |
| 92 | | hashss 14448 |
. . . . 5
⊢ (({𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ∈ V ∧ ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴)) ⊆ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) → (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) ≤ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 93 | 33, 91, 92 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (♯‘ran (𝑖 ∈ ℤ ↦ (𝑖 ↑ 𝐴))) ≤ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 94 | 29, 93 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ≤ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) |
| 95 | 15, 94 | jca 511 |
. 2
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ≤ ((od‘𝐺)‘𝐴) ∧ ((od‘𝐺)‘𝐴) ≤ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}))) |
| 96 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ⊆ 𝐵 |
| 97 | 96 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ⊆ 𝐵) |
| 98 | 9, 97 | ssfid 9301 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ∈ Fin) |
| 99 | | hashcl 14395 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ∈
ℕ0) |
| 100 | 98, 99 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ∈
ℕ0) |
| 101 | 100 | nn0red 12588 |
. . 3
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ∈ ℝ) |
| 102 | 14 | nnred 12281 |
. . 3
⊢ (𝜑 → ((od‘𝐺)‘𝐴) ∈ ℝ) |
| 103 | 101, 102 | letri3d 11403 |
. 2
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴) ↔ ((♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) ≤ ((od‘𝐺)‘𝐴) ∧ ((od‘𝐺)‘𝐴) ≤ (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})))) |
| 104 | 95, 103 | mpbird 257 |
1
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴)) |