Metamath Proof Explorer


Theorem ccats1val2

Description: Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Proof shortened by Alexander van der Vekens, 14-Oct-2018)

Ref Expression
Assertion ccats1val2 WWordVSVI=WW++⟨“S”⟩I=S

Proof

Step Hyp Ref Expression
1 simp1 WWordVSVI=WWWordV
2 s1cl SV⟨“S”⟩WordV
3 2 3ad2ant2 WWordVSVI=W⟨“S”⟩WordV
4 lencl WWordVW0
5 4 nn0zd WWordVW
6 elfzomin WWW..^W+1
7 5 6 syl WWordVWW..^W+1
8 s1len ⟨“S”⟩=1
9 8 oveq2i W+⟨“S”⟩=W+1
10 9 oveq2i W..^W+⟨“S”⟩=W..^W+1
11 7 10 eleqtrrdi WWordVWW..^W+⟨“S”⟩
12 11 adantr WWordVI=WWW..^W+⟨“S”⟩
13 eleq1 I=WIW..^W+⟨“S”⟩WW..^W+⟨“S”⟩
14 13 adantl WWordVI=WIW..^W+⟨“S”⟩WW..^W+⟨“S”⟩
15 12 14 mpbird WWordVI=WIW..^W+⟨“S”⟩
16 15 3adant2 WWordVSVI=WIW..^W+⟨“S”⟩
17 ccatval2 WWordV⟨“S”⟩WordVIW..^W+⟨“S”⟩W++⟨“S”⟩I=⟨“S”⟩IW
18 1 3 16 17 syl3anc WWordVSVI=WW++⟨“S”⟩I=⟨“S”⟩IW
19 oveq1 I=WIW=WW
20 19 3ad2ant3 WWordVSVI=WIW=WW
21 4 nn0cnd WWordVW
22 21 subidd WWordVWW=0
23 22 3ad2ant1 WWordVSVI=WWW=0
24 20 23 eqtrd WWordVSVI=WIW=0
25 24 fveq2d WWordVSVI=W⟨“S”⟩IW=⟨“S”⟩0
26 s1fv SV⟨“S”⟩0=S
27 26 3ad2ant2 WWordVSVI=W⟨“S”⟩0=S
28 18 25 27 3eqtrd WWordVSVI=WW++⟨“S”⟩I=S