Metamath Proof Explorer

Theorem ccatdmss

Description: The domain of a concatenated word is a superset of the domain of the first word. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses ccatdmss.1 ⊢ φ → A ∈ Word S
ccatdmss.2 ⊢ φ → B ∈ Word S
Assertion ccatdmss ⊢ φ → dom ⁡ A ⊆ dom ⁡ A ++ B

Proof

Step Hyp Ref Expression
1 ccatdmss.1 ⊢ φ → A ∈ Word S
2 ccatdmss.2 ⊢ φ → B ∈ Word S
3 lencl ⊢ A ∈ Word S → A ∈ ℕ 0
4 1 3 syl ⊢ φ → A ∈ ℕ 0
5 4 nn0zd ⊢ φ → A ∈ ℤ
6 ccatcl ⊢ A ∈ Word S ∧ B ∈ Word S → A ++ B ∈ Word S
7 1 2 6 syl2anc ⊢ φ → A ++ B ∈ Word S
8 lencl ⊢ A ++ B ∈ Word S → A ++ B ∈ ℕ 0
9 7 8 syl ⊢ φ → A ++ B ∈ ℕ 0
10 9 nn0zd ⊢ φ → A ++ B ∈ ℤ
11 4 nn0red ⊢ φ → A ∈ ℝ
12 lencl ⊢ B ∈ Word S → B ∈ ℕ 0
13 2 12 syl ⊢ φ → B ∈ ℕ 0
14 nn0addge1 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 → A ≤ A + B
15 11 13 14 syl2anc ⊢ φ → A ≤ A + B
16 ccatlen ⊢ A ∈ Word S ∧ B ∈ Word S → A ++ B = A + B
17 1 2 16 syl2anc ⊢ φ → A ++ B = A + B
18 15 17 breqtrrd ⊢ φ → A ≤ A ++ B
19 eluz2 ⊢ A ++ B ∈ ℤ ≥ A ↔ A ∈ ℤ ∧ A ++ B ∈ ℤ ∧ A ≤ A ++ B
20 5 10 18 19 syl3anbrc ⊢ φ → A ++ B ∈ ℤ ≥ A
21 fzoss2 ⊢ A ++ B ∈ ℤ ≥ A → 0 ..^ A ⊆ 0 ..^ A ++ B
22 20 21 syl ⊢ φ → 0 ..^ A ⊆ 0 ..^ A ++ B
23 eqidd ⊢ φ → A = A
24 23 1 wrdfd ⊢ φ → A : 0 ..^ A ⟶ S
25 24 fdmd ⊢ φ → dom ⁡ A = 0 ..^ A
26 eqidd ⊢ φ → A ++ B = A ++ B
27 26 7 wrdfd ⊢ φ → A ++ B : 0 ..^ A ++ B ⟶ S
28 27 fdmd ⊢ φ → dom ⁡ A ++ B = 0 ..^ A ++ B
29 22 25 28 3sstr4d ⊢ φ → dom ⁡ A ⊆ dom ⁡ A ++ B