| Step | Hyp | Ref
| Expression |
| 1 | | df-substr 14679 |
. . 3
⊢ substr =
(𝑠 ∈ V, 𝑏 ∈ (ℤ ×
ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅)) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦
if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅))) |
| 3 | | simprl 771 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉)) → 𝑠 = 𝑆) |
| 4 | | fveq2 6906 |
. . . . 5
⊢ (𝑏 = 〈𝐹, 𝐿〉 → (1st ‘𝑏) = (1st
‘〈𝐹, 𝐿〉)) |
| 5 | 4 | adantl 481 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉) → (1st ‘𝑏) = (1st
‘〈𝐹, 𝐿〉)) |
| 6 | | op1stg 8026 |
. . . . 5
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
(1st ‘〈𝐹, 𝐿〉) = 𝐹) |
| 7 | 6 | 3adant1 1131 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (1st
‘〈𝐹, 𝐿〉) = 𝐹) |
| 8 | 5, 7 | sylan9eqr 2799 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉)) → (1st ‘𝑏) = 𝐹) |
| 9 | | fveq2 6906 |
. . . . 5
⊢ (𝑏 = 〈𝐹, 𝐿〉 → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝐿〉)) |
| 10 | 9 | adantl 481 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉) → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝐿〉)) |
| 11 | | op2ndg 8027 |
. . . . 5
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
(2nd ‘〈𝐹, 𝐿〉) = 𝐿) |
| 12 | 11 | 3adant1 1131 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (2nd
‘〈𝐹, 𝐿〉) = 𝐿) |
| 13 | 10, 12 | sylan9eqr 2799 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉)) → (2nd ‘𝑏) = 𝐿) |
| 14 | | simp2 1138 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (1st ‘𝑏) = 𝐹) |
| 15 | | simp3 1139 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (2nd ‘𝑏) = 𝐿) |
| 16 | 14, 15 | oveq12d 7449 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → ((1st ‘𝑏)..^(2nd ‘𝑏)) = (𝐹..^𝐿)) |
| 17 | | simp1 1137 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → 𝑠 = 𝑆) |
| 18 | 17 | dmeqd 5916 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → dom 𝑠 = dom 𝑆) |
| 19 | 16, 18 | sseq12d 4017 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠 ↔ (𝐹..^𝐿) ⊆ dom 𝑆)) |
| 20 | 15, 14 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → ((2nd ‘𝑏) − (1st
‘𝑏)) = (𝐿 − 𝐹)) |
| 21 | 20 | oveq2d 7447 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (0..^((2nd ‘𝑏) − (1st
‘𝑏))) = (0..^(𝐿 − 𝐹))) |
| 22 | 14 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (𝑥 + (1st ‘𝑏)) = (𝑥 + 𝐹)) |
| 23 | 17, 22 | fveq12d 6913 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (𝑠‘(𝑥 + (1st ‘𝑏))) = (𝑆‘(𝑥 + 𝐹))) |
| 24 | 21, 23 | mpteq12dv 5233 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹)))) |
| 25 | 19, 24 | ifbieq1d 4550 |
. . 3
⊢ ((𝑠 = 𝑆 ∧ (1st ‘𝑏) = 𝐹 ∧ (2nd ‘𝑏) = 𝐿) → if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) |
| 26 | 3, 8, 13, 25 | syl3anc 1373 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝐿〉)) → if(((1st
‘𝑏)..^(2nd
‘𝑏)) ⊆ dom
𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) |
| 27 | | elex 3501 |
. . 3
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
| 28 | 27 | 3ad2ant1 1134 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝑆 ∈ V) |
| 29 | | opelxpi 5722 |
. . 3
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ)) |
| 30 | 29 | 3adant1 1131 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ)) |
| 31 | | ovex 7464 |
. . . . 5
⊢
(0..^(𝐿 −
𝐹)) ∈
V |
| 32 | 31 | mptex 7243 |
. . . 4
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))) ∈ V |
| 33 | | 0ex 5307 |
. . . 4
⊢ ∅
∈ V |
| 34 | 32, 33 | ifex 4576 |
. . 3
⊢ if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅) ∈ V |
| 35 | 34 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅) ∈ V) |
| 36 | 2, 26, 28, 30, 35 | ovmpod 7585 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) |