Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑧 = 0 → (𝑅‘𝑧) = (𝑅‘0)) |
2 | 1 | fveq2d 6107 |
. . . . 5
⊢ (𝑧 = 0 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) |
3 | 2 | eqeq1d 2612 |
. . . 4
⊢ (𝑧 = 0 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0)))) |
4 | 3 | imbi2d 329 |
. . 3
⊢ (𝑧 = 0 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))))) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑧 = 𝑘 → (𝑅‘𝑧) = (𝑅‘𝑘)) |
6 | 5 | fveq2d 6107 |
. . . . 5
⊢ (𝑧 = 𝑘 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝑘))) |
7 | 6 | eqeq1d 2612 |
. . . 4
⊢ (𝑧 = 𝑘 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
8 | 7 | imbi2d 329 |
. . 3
⊢ (𝑧 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))))) |
9 | | fveq2 6103 |
. . . . . 6
⊢ (𝑧 = (𝑘 + 1) → (𝑅‘𝑧) = (𝑅‘(𝑘 + 1))) |
10 | 9 | fveq2d 6107 |
. . . . 5
⊢ (𝑧 = (𝑘 + 1) → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘(𝑘 + 1)))) |
11 | 10 | eqeq1d 2612 |
. . . 4
⊢ (𝑧 = (𝑘 + 1) → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
12 | 11 | imbi2d 329 |
. . 3
⊢ (𝑧 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
13 | | fveq2 6103 |
. . . . . 6
⊢ (𝑧 = 𝐾 → (𝑅‘𝑧) = (𝑅‘𝐾)) |
14 | 13 | fveq2d 6107 |
. . . . 5
⊢ (𝑧 = 𝐾 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝐾))) |
15 | 14 | eqeq1d 2612 |
. . . 4
⊢ (𝑧 = 𝐾 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
16 | 15 | imbi2d 329 |
. . 3
⊢ (𝑧 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))))) |
17 | | eqidd 2611 |
. . 3
⊢ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))) |
18 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
19 | | alginv.1 |
. . . . . . . . . 10
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴})) |
20 | | 0zd 11266 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
21 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
22 | | alginv.2 |
. . . . . . . . . . 11
⊢ 𝐹:𝑆⟶𝑆 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
24 | 18, 19, 20, 21, 23 | algrp1 15125 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
25 | 24 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
26 | 18, 19, 20, 21, 23 | algrf 15124 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
27 | 26 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
28 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑅‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝑅‘𝑘))) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
30 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘𝑥) = (𝐼‘(𝑅‘𝑘))) |
31 | 29, 30 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅‘𝑘) → ((𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥) ↔ (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘)))) |
32 | | alginv.4 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥)) |
33 | 31, 32 | vtoclga 3245 |
. . . . . . . . 9
⊢ ((𝑅‘𝑘) ∈ 𝑆 → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
34 | 27, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
35 | 25, 34 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘𝑘))) |
36 | 35 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
37 | 36 | biimprd 237 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
38 | 37 | expcom 450 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
39 | 38 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))) → (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
40 | 4, 8, 12, 16, 17, 39 | nn0ind 11348 |
. 2
⊢ (𝐾 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
41 | 40 | impcom 445 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0) → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))) |