Metamath Proof Explorer

Theorem lswccatn0lsw

Description: The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion lswccatn0lsw ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → lastS ⁡ A ++ B = lastS ⁡ B

Proof

Step Hyp Ref Expression
1 ccatlen ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = A + B
2 1 oveq1d ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B − 1 = A + B - 1
3 2 3adant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B − 1 = A + B - 1
4 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
5 4 nn0zd ⊢ A ∈ Word V → A ∈ ℤ
6 lennncl ⊢ B ∈ Word V ∧ B ≠ ∅ → B ∈ ℕ
7 simpl ⊢ A ∈ ℤ ∧ B ∈ ℕ → A ∈ ℤ
8 nnz ⊢ B ∈ ℕ → B ∈ ℤ
9 zaddcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + B ∈ ℤ
10 8 9 sylan2 ⊢ A ∈ ℤ ∧ B ∈ ℕ → A + B ∈ ℤ
11 zre ⊢ A ∈ ℤ → A ∈ ℝ
12 nnrp ⊢ B ∈ ℕ → B ∈ ℝ +
13 ltaddrp ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A < A + B
14 11 12 13 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℕ → A < A + B
15 7 10 14 3jca ⊢ A ∈ ℤ ∧ B ∈ ℕ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
16 5 6 15 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
17 16 3impb ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
18 fzolb ⊢ A ∈ A ..^ A + B ↔ A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
19 17 18 sylibr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ A ..^ A + B
20 fzoend ⊢ A ∈ A ..^ A + B → A + B - 1 ∈ A ..^ A + B
21 19 20 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A + B - 1 ∈ A ..^ A + B
22 3 21 eqeltrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B − 1 ∈ A ..^ A + B
23 ccatval2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ++ B − 1 ∈ A ..^ A + B → A ++ B ⁡ A ++ B − 1 = B ⁡ A ++ B - 1 - A
24 22 23 syld3an3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B ⁡ A ++ B − 1 = B ⁡ A ++ B - 1 - A
25 2 oveq1d ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B - 1 - A = A + B - 1 - A
26 4 nn0cnd ⊢ A ∈ Word V → A ∈ ℂ
27 lencl ⊢ B ∈ Word V → B ∈ ℕ 0
28 27 nn0cnd ⊢ B ∈ Word V → B ∈ ℂ
29 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
30 1cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 ∈ ℂ
31 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
32 29 30 31 sub32d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - 1 - A = A + B - A - 1
33 pncan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B
34 33 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A - 1 = B − 1
35 32 34 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - 1 - A = B − 1
36 26 28 35 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V → A + B - 1 - A = B − 1
37 25 36 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B - 1 - A = B − 1
38 37 3adant3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B - 1 - A = B − 1
39 38 fveq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → B ⁡ A ++ B - 1 - A = B ⁡ B − 1
40 24 39 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B ⁡ A ++ B − 1 = B ⁡ B − 1
41 ovex ⊢ A ++ B ∈ V
42 lsw ⊢ A ++ B ∈ V → lastS ⁡ A ++ B = A ++ B ⁡ A ++ B − 1
43 41 42 mp1i ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → lastS ⁡ A ++ B = A ++ B ⁡ A ++ B − 1
44 lsw ⊢ B ∈ Word V → lastS ⁡ B = B ⁡ B − 1
45 44 3ad2ant2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → lastS ⁡ B = B ⁡ B − 1
46 40 43 45 3eqtr4d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → lastS ⁡ A ++ B = lastS ⁡ B