This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑆 ∈ Word 𝐵 → ( ∅ ++ 𝑆 ) = 𝑆 )

Proof

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