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 ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) , ∅ ) )
2	1	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) , ∅ ) ) )
3		simprl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) ) → 𝑠 = 𝑆 )
4		fveq2	⊢ ( 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ ⟨ 𝐹 , 𝐿 ⟩ ) )
5	4	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ ⟨ 𝐹 , 𝐿 ⟩ ) )
6		op1stg	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1^st ‘ ⟨ 𝐹 , 𝐿 ⟩ ) = 𝐹 )
7	6	3adant1	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1^st ‘ ⟨ 𝐹 , 𝐿 ⟩ ) = 𝐹 )
8	5 7	sylan9eqr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) ) → ( 1^st ‘ 𝑏 ) = 𝐹 )
9		fveq2	⊢ ( 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝐿 ⟩ ) )
10	9	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝐿 ⟩ ) )
11		op2ndg	⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐿 ⟩ ) = 𝐿 )
12	11	3adant1	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐿 ⟩ ) = 𝐿 )
13	10 12	sylan9eqr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) ) → ( 2^nd ‘ 𝑏 ) = 𝐿 )
14		simp2	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 1^st ‘ 𝑏 ) = 𝐹 )
15		simp3	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 2^nd ‘ 𝑏 ) = 𝐿 )
16	14 15	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) = ( 𝐹 ..^ 𝐿 ) )
17		simp1	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → 𝑠 = 𝑆 )
18	17	dmeqd	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → dom 𝑠 = dom 𝑆 )
19	16 18	sseq12d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 ↔ ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 ) )
20	15 14	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) = ( 𝐿 − 𝐹 ) )
21	20	oveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) = ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
22	14	oveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑥 + ( 1^st ‘ 𝑏 ) ) = ( 𝑥 + 𝐹 ) )
23	17 22	fveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) = ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) )
24	21 23	mpteq12dv	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )
25	19 24	ifbieq1d	⊢ ( ( 𝑠 = 𝑆 ∧ ( 1^st ‘ 𝑏 ) = 𝐹 ∧ ( 2^nd ‘ 𝑏 ) = 𝐿 ) → if ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) , ∅ ) = if ( ( 𝐹 ..^ 𝐿 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )
26	3 8 13 25	syl3anc	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝐿 ⟩ ) ) → if ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) , ∅ ) = 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 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) , ∅ ) )

Metamath Proof Explorer

Theorem swrdval

Proof