Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 𝐹 ∈ 𝑉) |
2 | | itcoval 45425 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
3 | 2 | fveq1d 6653 |
. . 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 12305 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
6 | | simp2 1135 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 𝑌 ∈
ℕ0) |
7 | | eqid 2759 |
. . 3
⊢ (𝑌 + 1) = (𝑌 + 1) |
8 | 2 | adantr 485 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
(IterComp‘𝐹) =
seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
9 | 8 | fveq1d 6653 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
((IterComp‘𝐹)‘𝑌) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌)) |
10 | 9 | eqeq1d 2761 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) →
(((IterComp‘𝐹)‘𝑌) = 𝐺 ↔ (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌) = 𝐺)) |
11 | 10 | biimp3a 1467 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘𝑌) = 𝐺) |
12 | | eqidd 2760 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) |
13 | | nn0p1gt0 11948 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℕ0
→ 0 < (𝑌 +
1)) |
14 | 13 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → 0 < (𝑌 + 1)) |
15 | 14 | gt0ne0d 11227 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑌 + 1) ≠ 0) |
16 | 15 | adantr 485 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → (𝑌 + 1) ≠ 0) |
17 | | neeq1 3011 |
. . . . . . . 8
⊢ (𝑖 = (𝑌 + 1) → (𝑖 ≠ 0 ↔ (𝑌 + 1) ≠ 0)) |
18 | 17 | adantl 486 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → (𝑖 ≠ 0 ↔ (𝑌 + 1) ≠ 0)) |
19 | 16, 18 | mpbird 260 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → 𝑖 ≠ 0) |
20 | 19 | neneqd 2954 |
. . . . 5
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → ¬ 𝑖 = 0) |
21 | 20 | iffalsed 4424 |
. . . 4
⊢ (((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) ∧ 𝑖 = (𝑌 + 1)) → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
22 | | peano2nn0 11959 |
. . . . 5
⊢ (𝑌 ∈ ℕ0
→ (𝑌 + 1) ∈
ℕ0) |
23 | 22 | 3ad2ant2 1132 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (𝑌 + 1) ∈
ℕ0) |
24 | 12, 21, 23, 1 | fvmptd 6759 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → ((𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))‘(𝑌 + 1)) = 𝐹) |
25 | 5, 6, 7, 11, 24 | seqp1d 13420 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |
26 | 4, 25 | eqtrd 2794 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧
((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |