Metamath Proof Explorer


Theorem swrdval

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

Ref Expression
Assertion swrdval SVFLSsubstrFL=ifF..^LdomSx0..^LFSx+F

Proof

Step Hyp Ref Expression
1 df-substr substr=sV,b×if1stb..^2ndbdomsx0..^2ndb1stbsx+1stb
2 1 a1i SVFLsubstr=sV,b×if1stb..^2ndbdomsx0..^2ndb1stbsx+1stb
3 simprl SVFLs=Sb=FLs=S
4 fveq2 b=FL1stb=1stFL
5 4 adantl s=Sb=FL1stb=1stFL
6 op1stg FL1stFL=F
7 6 3adant1 SVFL1stFL=F
8 5 7 sylan9eqr SVFLs=Sb=FL1stb=F
9 fveq2 b=FL2ndb=2ndFL
10 9 adantl s=Sb=FL2ndb=2ndFL
11 op2ndg FL2ndFL=L
12 11 3adant1 SVFL2ndFL=L
13 10 12 sylan9eqr SVFLs=Sb=FL2ndb=L
14 simp2 s=S1stb=F2ndb=L1stb=F
15 simp3 s=S1stb=F2ndb=L2ndb=L
16 14 15 oveq12d s=S1stb=F2ndb=L1stb..^2ndb=F..^L
17 simp1 s=S1stb=F2ndb=Ls=S
18 17 dmeqd s=S1stb=F2ndb=Ldoms=domS
19 16 18 sseq12d s=S1stb=F2ndb=L1stb..^2ndbdomsF..^LdomS
20 15 14 oveq12d s=S1stb=F2ndb=L2ndb1stb=LF
21 20 oveq2d s=S1stb=F2ndb=L0..^2ndb1stb=0..^LF
22 14 oveq2d s=S1stb=F2ndb=Lx+1stb=x+F
23 17 22 fveq12d s=S1stb=F2ndb=Lsx+1stb=Sx+F
24 21 23 mpteq12dv s=S1stb=F2ndb=Lx0..^2ndb1stbsx+1stb=x0..^LFSx+F
25 19 24 ifbieq1d s=S1stb=F2ndb=Lif1stb..^2ndbdomsx0..^2ndb1stbsx+1stb=ifF..^LdomSx0..^LFSx+F
26 3 8 13 25 syl3anc SVFLs=Sb=FLif1stb..^2ndbdomsx0..^2ndb1stbsx+1stb=ifF..^LdomSx0..^LFSx+F
27 elex SVSV
28 27 3ad2ant1 SVFLSV
29 opelxpi FLFL×
30 29 3adant1 SVFLFL×
31 ovex 0..^LFV
32 31 mptex x0..^LFSx+FV
33 0ex V
34 32 33 ifex ifF..^LdomSx0..^LFSx+FV
35 34 a1i SVFLifF..^LdomSx0..^LFSx+FV
36 2 26 28 30 35 ovmpod SVFLSsubstrFL=ifF..^LdomSx0..^LFSx+F