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 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) = ( lastS ‘ 𝐵 ) )

Proof

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