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

Metamath Proof Explorer

Theorem ccatval21sw

Description: The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion ccatval21sw ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 1 nn0zd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
3 lennncl ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
4 simpl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
5 nnz ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → ( ♯ ‘ 𝐵 ) ∈ ℤ )
6 zaddcl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
7 5 6 sylan2 ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
8 nngt0 ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → 0 < ( ♯ ‘ 𝐵 ) )
9 8 adantl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → 0 < ( ♯ ‘ 𝐵 ) )
10 nnre ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → ( ♯ ‘ 𝐵 ) ∈ ℝ )
11 zre ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( ♯ ‘ 𝐴 ) ∈ ℝ )
12 ltaddpos ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℝ ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ ) → ( 0 < ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
13 10 11 12 syl2anr ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 0 < ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
14 9 13 mpbid ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
15 4 7 14 3jca ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
16 2 3 15 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ ( 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
17 16 3impb ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
18 fzolb ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) < ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
19 17 18 sylibr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
20 ccatval2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐴 ) ) ) )
21 19 20 syld3an3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐴 ) ) ) )
22 1 nn0cnd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
23 22 subidd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐴 ) ) = 0 )
24 23 fveq2d ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐵 ‘ ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ 0 ) )
25 24 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( 𝐵 ‘ ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ 0 ) )
26 21 25 eqtrd ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) )