Metamath Proof Explorer


Theorem swrdval2

Description: Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdval2 SWordAF0LL0SSsubstrFL=x0..^LFSx+F

Proof

Step Hyp Ref Expression
1 simp1 SWordAF0LL0SSWordA
2 elfzelz F0LF
3 2 3ad2ant2 SWordAF0LL0SF
4 elfzelz L0SL
5 4 3ad2ant3 SWordAF0LL0SL
6 swrdval SWordAFLSsubstrFL=ifF..^LdomSx0..^LFSx+F
7 1 3 5 6 syl3anc SWordAF0LL0SSsubstrFL=ifF..^LdomSx0..^LFSx+F
8 elfzuz F0LF0
9 8 3ad2ant2 SWordAF0LL0SF0
10 fzoss1 F0F..^L0..^L
11 9 10 syl SWordAF0LL0SF..^L0..^L
12 elfzuz3 L0SSL
13 12 3ad2ant3 SWordAF0LL0SSL
14 fzoss2 SL0..^L0..^S
15 13 14 syl SWordAF0LL0S0..^L0..^S
16 11 15 sstrd SWordAF0LL0SF..^L0..^S
17 wrddm SWordAdomS=0..^S
18 17 3ad2ant1 SWordAF0LL0SdomS=0..^S
19 16 18 sseqtrrd SWordAF0LL0SF..^LdomS
20 19 iftrued SWordAF0LL0SifF..^LdomSx0..^LFSx+F=x0..^LFSx+F
21 7 20 eqtrd SWordAF0LL0SSsubstrFL=x0..^LFSx+F