| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 𝐹 ∈ 𝑉) |
| 2 | | itcoval 48582 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
| 3 | 2 | fveq1d 6908 |
. . 3
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘(𝑌 + 1)) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘(𝑌 + 1))) |
| 4 | 1, 3 | syl 17 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘(𝑌 + 1))) |
| 5 | | nn0uz 12920 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
| 6 | | simp2 1138 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 𝑌 ∈
ℕ0) |
| 7 | | eqid 2737 |
. . 3
⊢ (𝑌 + 1) = (𝑌 + 1) |
| 8 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
(IterComp‘𝐹) =
seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
| 9 | 8 | fveq1d 6908 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
((IterComp‘𝐹)‘𝑌) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌)) |
| 10 | 9 | eqeq1d 2739 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
(((IterComp‘𝐹)‘𝑌) = 𝐺 ↔ (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌) = 𝐺)) |
| 11 | 10 | biimp3a 1471 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌) = 𝐺) |
| 12 | | eqidd 2738 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) |
| 13 | | nn0p1gt0 12555 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℕ0
→ 0 < (𝑌 +
1)) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 0 < (𝑌 + 1)) |
| 15 | 14 | gt0ne0d 11827 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑌 + 1) ≠ 0) |
| 16 | 15 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → (𝑌 + 1) ≠ 0) |
| 17 | | neeq1 3003 |
. . . . . . . 8
⊢ (𝑖 = (𝑌 + 1) → (𝑖 ≠ 0 ↔ (𝑌 + 1) ≠ 0)) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → (𝑖 ≠ 0 ↔ (𝑌 + 1) ≠ 0)) |
| 19 | 16, 18 | mpbird 257 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → 𝑖 ≠ 0) |
| 20 | 19 | neneqd 2945 |
. . . . 5
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → ¬ 𝑖 = 0) |
| 21 | 20 | iffalsed 4536 |
. . . 4
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
| 22 | | peano2nn0 12566 |
. . . . 5
⊢ (𝑌 ∈ ℕ0
→ (𝑌 + 1) ∈
ℕ0) |
| 23 | 22 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑌 + 1) ∈
ℕ0) |
| 24 | 12, 21, 23, 1 | fvmptd 7023 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → ((𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))‘(𝑌 + 1)) = 𝐹) |
| 25 | 5, 6, 7, 11, 24 | seqp1d 14059 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |
| 26 | 4, 25 | eqtrd 2777 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |