Metamath Proof Explorer

Theorem ccatlid

Description: Concatenation of a word by the empty word on the left. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatlid ⊢S∈WordB→∅++S=S

Proof

Step Hyp Ref Expression
1 wrd0 ⊢∅∈WordB
2 ccatvalfn ⊢∅∈WordB∧S∈WordB→∅++SFn0..^∅+S
3 1 2 mpan ⊢S∈WordB→∅++SFn0..^∅+S
4 hash0 ⊢∅=0
5 4 oveq1i ⊢∅+S=0+S
6 lencl ⊢S∈WordB→S∈ℕ0
7 6 nn0cnd ⊢S∈WordB→S∈ℂ
8 7 addlidd ⊢S∈WordB→0+S=S
9 5 8 eqtrid ⊢S∈WordB→∅+S=S
10 9 eqcomd ⊢S∈WordB→S=∅+S
11 10 oveq2d ⊢S∈WordB→0..^S=0..^∅+S
12 11 fneq2d ⊢S∈WordB→∅++SFn0..^S↔∅++SFn0..^∅+S
13 3 12 mpbird ⊢S∈WordB→∅++SFn0..^S
14 wrdfn ⊢S∈WordB→SFn0..^S
15 4 a1i ⊢S∈WordB→∅=0
16 15 9 oveq12d ⊢S∈WordB→∅..^∅+S=0..^S
17 16 eleq2d ⊢S∈WordB→x∈∅..^∅+S↔x∈0..^S
18 17 biimpar ⊢S∈WordB∧x∈0..^S→x∈∅..^∅+S
19 ccatval2 ⊢∅∈WordB∧S∈WordB∧x∈∅..^∅+S→∅++S⁡x=S⁡x−∅
20 1 19 mp3an1 ⊢S∈WordB∧x∈∅..^∅+S→∅++S⁡x=S⁡x−∅
21 18 20 syldan ⊢S∈WordB∧x∈0..^S→∅++S⁡x=S⁡x−∅
22 4 oveq2i ⊢x−∅=x−0
23 elfzoelz ⊢x∈0..^S→x∈ℤ
24 23 adantl ⊢S∈WordB∧x∈0..^S→x∈ℤ
25 24 zcnd ⊢S∈WordB∧x∈0..^S→x∈ℂ
26 25 subid1d ⊢S∈WordB∧x∈0..^S→x−0=x
27 22 26 eqtrid ⊢S∈WordB∧x∈0..^S→x−∅=x
28 27 fveq2d ⊢S∈WordB∧x∈0..^S→S⁡x−∅=S⁡x
29 21 28 eqtrd ⊢S∈WordB∧x∈0..^S→∅++S⁡x=S⁡x
30 13 14 29 eqfnfvd ⊢S∈WordB→∅++S=S