Step |
Hyp |
Ref |
Expression |
1 |
|
df-substr |
⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ) |
2 |
1
|
a1i |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ) ) |
3 |
|
simprl |
⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) ) → 𝑠 = 𝑆 ) |
4 |
|
fveq2 |
⊢ ( 𝑏 = 〈 𝐹 , 𝐿 〉 → ( 1st ‘ 𝑏 ) = ( 1st ‘ 〈 𝐹 , 𝐿 〉 ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) → ( 1st ‘ 𝑏 ) = ( 1st ‘ 〈 𝐹 , 𝐿 〉 ) ) |
6 |
|
op1stg |
⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1st ‘ 〈 𝐹 , 𝐿 〉 ) = 𝐹 ) |
7 |
6
|
3adant1 |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1st ‘ 〈 𝐹 , 𝐿 〉 ) = 𝐹 ) |
8 |
5 7
|
sylan9eqr |
⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) ) → ( 1st ‘ 𝑏 ) = 𝐹 ) |
9 |
|
fveq2 |
⊢ ( 𝑏 = 〈 𝐹 , 𝐿 〉 → ( 2nd ‘ 𝑏 ) = ( 2nd ‘ 〈 𝐹 , 𝐿 〉 ) ) |
10 |
9
|
adantl |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) → ( 2nd ‘ 𝑏 ) = ( 2nd ‘ 〈 𝐹 , 𝐿 〉 ) ) |
11 |
|
op2ndg |
⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 2nd ‘ 〈 𝐹 , 𝐿 〉 ) = 𝐿 ) |
12 |
11
|
3adant1 |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 2nd ‘ 〈 𝐹 , 𝐿 〉 ) = 𝐿 ) |
13 |
10 12
|
sylan9eqr |
⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) ) → ( 2nd ‘ 𝑏 ) = 𝐿 ) |
14 |
|
simp2 |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 1st ‘ 𝑏 ) = 𝐹 ) |
15 |
|
simp3 |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 2nd ‘ 𝑏 ) = 𝐿 ) |
16 |
14 15
|
oveq12d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) = ( 𝐹 ..^ 𝐿 ) ) |
17 |
|
simp1 |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → 𝑠 = 𝑆 ) |
18 |
17
|
dmeqd |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → dom 𝑠 = dom 𝑆 ) |
19 |
16 18
|
sseq12d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 ↔ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) ) |
20 |
15 14
|
oveq12d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) = ( 𝐿 − 𝐹 ) ) |
21 |
20
|
oveq2d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) = ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) |
22 |
14
|
oveq2d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑥 + ( 1st ‘ 𝑏 ) ) = ( 𝑥 + 𝐹 ) ) |
23 |
17 22
|
fveq12d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) = ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) |
24 |
21 23
|
mpteq12dv |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ) |
25 |
19 24
|
ifbieq1d |
⊢ ( ( 𝑠 = 𝑆 ∧ ( 1st ‘ 𝑏 ) = 𝐹 ∧ ( 2nd ‘ 𝑏 ) = 𝐿 ) → if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ) |
26 |
3 8 13 25
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = 〈 𝐹 , 𝐿 〉 ) ) → if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ) |
27 |
|
elex |
⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V ) |
28 |
27
|
3ad2ant1 |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝑆 ∈ V ) |
29 |
|
opelxpi |
⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 〈 𝐹 , 𝐿 〉 ∈ ( ℤ × ℤ ) ) |
30 |
29
|
3adant1 |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 〈 𝐹 , 𝐿 〉 ∈ ( ℤ × ℤ ) ) |
31 |
|
ovex |
⊢ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ∈ V |
32 |
31
|
mptex |
⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ∈ V |
33 |
|
0ex |
⊢ ∅ ∈ V |
34 |
32 33
|
ifex |
⊢ if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ∈ V |
35 |
34
|
a1i |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ∈ V ) |
36 |
2 26 28 30 35
|
ovmpod |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr 〈 𝐹 , 𝐿 〉 ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) ) |