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 ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑆 )
ccatdmss.2 ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑆 )
Assertion ccatdmss ( 𝜑 → dom 𝐴 ⊆ dom ( 𝐴 ++ 𝐵 ) )

Proof

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