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 ∈ Word B → ∅ ++ S = S

Proof

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