| Step | Hyp | Ref
| Expression |
| 1 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑧 = 0 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) |
| 2 | 1 | eqeq1d 2739 |
. . . 4
⊢ (𝑧 = 0 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0)))) |
| 3 | 2 | imbi2d 340 |
. . 3
⊢ (𝑧 = 0 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))))) |
| 4 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑧 = 𝑘 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝑘))) |
| 5 | 4 | eqeq1d 2739 |
. . . 4
⊢ (𝑧 = 𝑘 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑧 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))))) |
| 7 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑧 = (𝑘 + 1) → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘(𝑘 + 1)))) |
| 8 | 7 | eqeq1d 2739 |
. . . 4
⊢ (𝑧 = (𝑘 + 1) → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
| 9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑧 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
| 10 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑧 = 𝐾 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘𝐾))) |
| 11 | 10 | eqeq1d 2739 |
. . . 4
⊢ (𝑧 = 𝐾 → ((𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑧 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑧)) = (𝐼‘(𝑅‘0))) ↔ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))))) |
| 13 | | eqidd 2738 |
. . 3
⊢ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘0)) = (𝐼‘(𝑅‘0))) |
| 14 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 15 | | alginv.1 |
. . . . . . . . . 10
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴})) |
| 16 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
| 17 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
| 18 | | alginv.2 |
. . . . . . . . . . 11
⊢ 𝐹:𝑆⟶𝑆 |
| 19 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
| 20 | 14, 15, 16, 17, 19 | algrp1 16611 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
| 22 | 14, 15, 16, 17, 19 | algrf 16610 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
| 23 | 22 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
| 24 | | 2fveq3 6911 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘(𝑅‘𝑘)))) |
| 25 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑅‘𝑘) → (𝐼‘𝑥) = (𝐼‘(𝑅‘𝑘))) |
| 26 | 24, 25 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅‘𝑘) → ((𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥) ↔ (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘)))) |
| 27 | | alginv.3 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥)) |
| 28 | 26, 27 | vtoclga 3577 |
. . . . . . . . 9
⊢ ((𝑅‘𝑘) ∈ 𝑆 → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
| 29 | 23, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝐹‘(𝑅‘𝑘))) = (𝐼‘(𝑅‘𝑘))) |
| 30 | 21, 29 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘𝑘))) |
| 31 | 30 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)) ↔ (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)))) |
| 32 | 31 | biimprd 248 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0)))) |
| 33 | 32 | expcom 413 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → ((𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0)) → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
| 34 | 33 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝑘)) = (𝐼‘(𝑅‘0))) → (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘(𝑘 + 1))) = (𝐼‘(𝑅‘0))))) |
| 35 | 3, 6, 9, 12, 13, 34 | nn0ind 12713 |
. 2
⊢ (𝐾 ∈ ℕ0
→ (𝐴 ∈ 𝑆 → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))) |
| 36 | 35 | impcom 407 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0) → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))) |