Step | Hyp | Ref
| Expression |
1 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = 0 → (𝑅‘𝑧) = (𝑅‘0)) |
2 | 1 | fveq2d 5182 |
. . . . 5
⊢ (𝑧 = 0 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) |
3 | 2 | eqeq1d 2048 |
. . . 4
⊢ (𝑧 = 0 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0)))) |
4 | 3 | imbi2d 219 |
. . 3
⊢ (𝑧 = 0 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))))) |
5 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = 𝑘 → (𝑅‘𝑧) = (𝑅‘𝑘)) |
6 | 5 | fveq2d 5182 |
. . . . 5
⊢ (𝑧 = 𝑘 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝑘))) |
7 | 6 | eqeq1d 2048 |
. . . 4
⊢ (𝑧 = 𝑘 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
8 | 7 | imbi2d 219 |
. . 3
⊢ (𝑧 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))))) |
9 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = (𝑘 + 1) → (𝑅‘𝑧) = (𝑅‘(𝑘 + 1))) |
10 | 9 | fveq2d 5182 |
. . . . 5
⊢ (𝑧 = (𝑘 + 1) → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘(𝑘 + 1)))) |
11 | 10 | eqeq1d 2048 |
. . . 4
⊢ (𝑧 = (𝑘 + 1) → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
12 | 11 | imbi2d 219 |
. . 3
⊢ (𝑧 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
13 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = 𝐾 → (𝑅‘𝑧) = (𝑅‘𝐾)) |
14 | 13 | fveq2d 5182 |
. . . . 5
⊢ (𝑧 = 𝐾 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝐾))) |
15 | 14 | eqeq1d 2048 |
. . . 4
⊢ (𝑧 = 𝐾 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
16 | 15 | imbi2d 219 |
. . 3
⊢ (𝑧 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))))) |
17 | | eqidd 2041 |
. . 3
⊢ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))) |
18 | | nn0uz 8507 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
19 | | alginv.1 |
. . . . . . . . . 10
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴}), 𝑆) |
20 | | 0zd 8257 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
21 | | id 19 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
22 | | alginv.2 |
. . . . . . . . . . 11
⊢ 𝐹:𝑆⟶𝑆 |
23 | 22 | a1i 9 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
24 | | alginv.s |
. . . . . . . . . . 11
⊢ 𝑆 ∈ 𝑉 |
25 | 24 | a1i 9 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝑆 ∈ 𝑉) |
26 | 18, 19, 20, 21, 23, 25 | ialgrp1 9885 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
27 | 26 | fveq2d 5182 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
28 | 18, 19, 20, 21, 23, 25 | ialgrf 9884 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
29 | 28 | ffvelrnda 5302 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
30 | | fveq2 5178 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑅‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝑅‘𝑘))) |
31 | 30 | fveq2d 5182 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
32 | | fveq2 5178 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘𝑥) = (𝐼‘(𝑅‘𝑘))) |
33 | 31, 32 | eqeq12d 2054 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅‘𝑘) → ((𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥) ↔ (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘)))) |
34 | | alginv.4 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥)) |
35 | 33, 34 | vtoclga 2619 |
. . . . . . . . 9
⊢ ((𝑅‘𝑘) ∈ 𝑆 → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
36 | 29, 35 | syl 14 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
37 | 27, 36 | eqtrd 2072 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘𝑘))) |
38 | 37 | eqeq1d 2048 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
39 | 38 | biimprd 147 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
40 | 39 | expcom 109 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
41 | 40 | a2d 23 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))) → (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
42 | 4, 8, 12, 16, 17, 41 | nn0ind 8352 |
. 2
⊢ (𝐾 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
43 | 42 | impcom 116 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0) → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))) |