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∈WordV∧B∈WordV∧B≠∅→lastS⁡A++B=lastS⁡B

Proof

Step Hyp Ref Expression
1 ccatlen ⊢A∈WordV∧B∈WordV→A++B=A+B
2 1 oveq1d ⊢A∈WordV∧B∈WordV→A++B−1=A+B-1
3 2 3adant3 ⊢A∈WordV∧B∈WordV∧B≠∅→A++B−1=A+B-1
4 lencl ⊢A∈WordV→A∈ℕ0
5 4 nn0zd ⊢A∈WordV→A∈ℤ
6 lennncl ⊢B∈WordV∧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∈WordV∧B∈WordV∧B≠∅→A∈ℤ∧A+B∈ℤ∧A<A+B
17 16 3impb ⊢A∈WordV∧B∈WordV∧B≠∅→A∈ℤ∧A+B∈ℤ∧A<A+B
18 fzolb ⊢A∈A..^A+B↔A∈ℤ∧A+B∈ℤ∧A<A+B
19 17 18 sylibr ⊢A∈WordV∧B∈WordV∧B≠∅→A∈A..^A+B
20 fzoend ⊢A∈A..^A+B→A+B-1∈A..^A+B
21 19 20 syl ⊢A∈WordV∧B∈WordV∧B≠∅→A+B-1∈A..^A+B
22 3 21 eqeltrd ⊢A∈WordV∧B∈WordV∧B≠∅→A++B−1∈A..^A+B
23 ccatval2 ⊢A∈WordV∧B∈WordV∧A++B−1∈A..^A+B→A++B⁡A++B−1=B⁡A++B-1-A
24 22 23 syld3an3 ⊢A∈WordV∧B∈WordV∧B≠∅→A++B⁡A++B−1=B⁡A++B-1-A
25 2 oveq1d ⊢A∈WordV∧B∈WordV→A++B-1-A=A+B-1-A
26 4 nn0cnd ⊢A∈WordV→A∈ℂ
27 lencl ⊢B∈WordV→B∈ℕ0
28 27 nn0cnd ⊢B∈WordV→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∈WordV∧B∈WordV→A+B-1-A=B−1
37 25 36 eqtrd ⊢A∈WordV∧B∈WordV→A++B-1-A=B−1
38 37 3adant3 ⊢A∈WordV∧B∈WordV∧B≠∅→A++B-1-A=B−1
39 38 fveq2d ⊢A∈WordV∧B∈WordV∧B≠∅→B⁡A++B-1-A=B⁡B−1
40 24 39 eqtrd ⊢A∈WordV∧B∈WordV∧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∈WordV∧B∈WordV∧B≠∅→lastS⁡A++B=A++B⁡A++B−1
44 lsw ⊢B∈WordV→lastS⁡B=B⁡B−1
45 44 3ad2ant2 ⊢A∈WordV∧B∈WordV∧B≠∅→lastS⁡B=B⁡B−1
46 40 43 45 3eqtr4d ⊢A∈WordV∧B∈WordV∧B≠∅→lastS⁡A++B=lastS⁡B