Metamath Proof Explorer


Theorem swrdval

Description: Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion swrdval ( ( 𝑆𝑉𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )

Proof

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 ..^ ( 𝐿𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )