Metamath Proof Explorer

Theorem ccatalpha

Description: A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021)

Ref Expression
Assertion ccatalpha ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word S ↔ A ∈ Word S ∧ B ∈ Word S

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
2 1 eleq1d ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word S ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Word S
3 wrdf ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Word S → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ⟶ S
4 funmpt ⊢ Fun ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
5 fzofi ⊢ 0 ..^ A + B ∈ Fin
6 mptfi ⊢ 0 ..^ A + B ∈ Fin → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Fin
7 5 6 ax-mp ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Fin
8 hashfun ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Fin → Fun ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
9 7 8 mp1i ⊢ A ∈ Word V ∧ B ∈ Word V → Fun ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
10 4 9 mpbii ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
11 dmmptg ⊢ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ V → dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = 0 ..^ A + B
12 fvex ⊢ A ⁡ x ∈ V
13 fvex ⊢ B ⁡ x − A ∈ V
14 12 13 ifex ⊢ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ V
15 14 a1i ⊢ x ∈ 0 ..^ A + B → if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ V
16 11 15 mprg ⊢ dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = 0 ..^ A + B
17 16 fveq2i ⊢ dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = 0 ..^ A + B
18 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
19 lencl ⊢ B ∈ Word V → B ∈ ℕ 0
20 nn0addcl ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A + B ∈ ℕ 0
21 18 19 20 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V → A + B ∈ ℕ 0
22 hashfzo0 ⊢ A + B ∈ ℕ 0 → 0 ..^ A + B = A + B
23 21 22 syl ⊢ A ∈ Word V ∧ B ∈ Word V → 0 ..^ A + B = A + B
24 17 23 syl5eq ⊢ A ∈ Word V ∧ B ∈ Word V → dom ⁡ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = A + B
25 10 24 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = A + B
26 25 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V → 0 ..^ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = 0 ..^ A + B
27 26 feq2d ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ⟶ S ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ A + B ⟶ S
28 eqid ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
29 28 fmpt ⊢ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ A + B ⟶ S
30 simpl ⊢ A ∈ Word V ∧ B ∈ Word V → A ∈ Word V
31 nn0cn ⊢ A ∈ ℕ 0 → A ∈ ℂ
32 nn0cn ⊢ B ∈ ℕ 0 → B ∈ ℂ
33 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
34 31 32 33 syl2an ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A + B = B + A
35 nn0z ⊢ A ∈ ℕ 0 → A ∈ ℤ
36 35 anim1ci ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → B ∈ ℕ 0 ∧ A ∈ ℤ
37 nn0pzuz ⊢ B ∈ ℕ 0 ∧ A ∈ ℤ → B + A ∈ ℤ ≥ A
38 36 37 syl ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → B + A ∈ ℤ ≥ A
39 34 38 eqeltrd ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A + B ∈ ℤ ≥ A
40 18 19 39 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V → A + B ∈ ℤ ≥ A
41 fzoss2 ⊢ A + B ∈ ℤ ≥ A → 0 ..^ A ⊆ 0 ..^ A + B
42 40 41 syl ⊢ A ∈ Word V ∧ B ∈ Word V → 0 ..^ A ⊆ 0 ..^ A + B
43 42 sselda ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ A → y ∈ 0 ..^ A + B
44 eleq1 ⊢ x = y → x ∈ 0 ..^ A ↔ y ∈ 0 ..^ A
45 fveq2 ⊢ x = y → A ⁡ x = A ⁡ y
46 fvoveq1 ⊢ x = y → B ⁡ x − A = B ⁡ y − A
47 44 45 46 ifbieq12d ⊢ x = y → if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A
48 47 eleq1d ⊢ x = y → if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S ↔ if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A ∈ S
49 48 rspcv ⊢ y ∈ 0 ..^ A + B → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A ∈ S
50 43 49 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ A → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A ∈ S
51 iftrue ⊢ y ∈ 0 ..^ A → if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A = A ⁡ y
52 51 adantl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ A → if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A = A ⁡ y
53 52 eleq1d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ A → if y ∈ 0 ..^ A A ⁡ y B ⁡ y − A ∈ S ↔ A ⁡ y ∈ S
54 50 53 sylibd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ A → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → A ⁡ y ∈ S
55 54 impancom ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → y ∈ 0 ..^ A → A ⁡ y ∈ S
56 55 ralrimiv ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → ∀ y ∈ 0 ..^ A A ⁡ y ∈ S
57 iswrdsymb ⊢ A ∈ Word V ∧ ∀ y ∈ 0 ..^ A A ⁡ y ∈ S → A ∈ Word S
58 30 56 57 syl2an2r ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → A ∈ Word S
59 simpr ⊢ A ∈ Word V ∧ B ∈ Word V → B ∈ Word V
60 simpr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y ∈ 0 ..^ B
61 18 adantr ⊢ A ∈ Word V ∧ B ∈ Word V → A ∈ ℕ 0
62 61 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → A ∈ ℕ 0
63 elincfzoext ⊢ y ∈ 0 ..^ B ∧ A ∈ ℕ 0 → y + A ∈ 0 ..^ B + A
64 60 62 63 syl2anc ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y + A ∈ 0 ..^ B + A
65 18 nn0cnd ⊢ A ∈ Word V → A ∈ ℂ
66 19 nn0cnd ⊢ B ∈ Word V → B ∈ ℂ
67 65 66 33 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V → A + B = B + A
68 67 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V → 0 ..^ A + B = 0 ..^ B + A
69 68 eleq2d ⊢ A ∈ Word V ∧ B ∈ Word V → y + A ∈ 0 ..^ A + B ↔ y + A ∈ 0 ..^ B + A
70 69 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y + A ∈ 0 ..^ A + B ↔ y + A ∈ 0 ..^ B + A
71 64 70 mpbird ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y + A ∈ 0 ..^ A + B
72 eleq1 ⊢ x = y + A → x ∈ 0 ..^ A ↔ y + A ∈ 0 ..^ A
73 fveq2 ⊢ x = y + A → A ⁡ x = A ⁡ y + A
74 fvoveq1 ⊢ x = y + A → B ⁡ x − A = B ⁡ y + A - A
75 72 73 74 ifbieq12d ⊢ x = y + A → if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A
76 75 eleq1d ⊢ x = y + A → if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S ↔ if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A ∈ S
77 76 rspcv ⊢ y + A ∈ 0 ..^ A + B → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A ∈ S
78 71 77 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A ∈ S
79 18 nn0red ⊢ A ∈ Word V → A ∈ ℝ
80 79 adantr ⊢ A ∈ Word V ∧ B ∈ Word V → A ∈ ℝ
81 80 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → A ∈ ℝ
82 elfzoelz ⊢ y ∈ 0 ..^ B → y ∈ ℤ
83 82 zred ⊢ y ∈ 0 ..^ B → y ∈ ℝ
84 83 adantr ⊢ y ∈ 0 ..^ B ∧ A ∈ Word V ∧ B ∈ Word V → y ∈ ℝ
85 80 adantl ⊢ y ∈ 0 ..^ B ∧ A ∈ Word V ∧ B ∈ Word V → A ∈ ℝ
86 84 85 readdcld ⊢ y ∈ 0 ..^ B ∧ A ∈ Word V ∧ B ∈ Word V → y + A ∈ ℝ
87 86 ancoms ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y + A ∈ ℝ
88 elfzole1 ⊢ y ∈ 0 ..^ B → 0 ≤ y
89 88 adantl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → 0 ≤ y
90 addge02 ⊢ A ∈ ℝ ∧ y ∈ ℝ → 0 ≤ y ↔ A ≤ y + A
91 80 83 90 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → 0 ≤ y ↔ A ≤ y + A
92 89 91 mpbid ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → A ≤ y + A
93 81 87 92 lensymd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → ¬ y + A < A
94 93 intn3an3d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → ¬ y + A ∈ ℕ 0 ∧ A ∈ ℕ ∧ y + A < A
95 elfzo0 ⊢ y + A ∈ 0 ..^ A ↔ y + A ∈ ℕ 0 ∧ A ∈ ℕ ∧ y + A < A
96 94 95 sylnibr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → ¬ y + A ∈ 0 ..^ A
97 96 iffalsed ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A = B ⁡ y + A - A
98 97 eleq1d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A ∈ S ↔ B ⁡ y + A - A ∈ S
99 82 zcnd ⊢ y ∈ 0 ..^ B → y ∈ ℂ
100 65 adantr ⊢ A ∈ Word V ∧ B ∈ Word V → A ∈ ℂ
101 pncan ⊢ y ∈ ℂ ∧ A ∈ ℂ → y + A - A = y
102 99 100 101 syl2anr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → y + A - A = y
103 102 fveq2d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → B ⁡ y + A - A = B ⁡ y
104 103 eleq1d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → B ⁡ y + A - A ∈ S ↔ B ⁡ y ∈ S
105 104 biimpd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → B ⁡ y + A - A ∈ S → B ⁡ y ∈ S
106 98 105 sylbid ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → if y + A ∈ 0 ..^ A A ⁡ y + A B ⁡ y + A - A ∈ S → B ⁡ y ∈ S
107 78 106 syld ⊢ A ∈ Word V ∧ B ∈ Word V ∧ y ∈ 0 ..^ B → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → B ⁡ y ∈ S
108 107 impancom ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → y ∈ 0 ..^ B → B ⁡ y ∈ S
109 108 ralrimiv ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → ∀ y ∈ 0 ..^ B B ⁡ y ∈ S
110 iswrdsymb ⊢ B ∈ Word V ∧ ∀ y ∈ 0 ..^ B B ⁡ y ∈ S → B ∈ Word S
111 59 109 110 syl2an2r ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → B ∈ Word S
112 58 111 jca ⊢ A ∈ Word V ∧ B ∈ Word V ∧ ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → A ∈ Word S ∧ B ∈ Word S
113 112 ex ⊢ A ∈ Word V ∧ B ∈ Word V → ∀ x ∈ 0 ..^ A + B if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ S → A ∈ Word S ∧ B ∈ Word S
114 29 113 syl5bir ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ A + B ⟶ S → A ∈ Word S ∧ B ∈ Word S
115 27 114 sylbid ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A : 0 ..^ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ⟶ S → A ∈ Word S ∧ B ∈ Word S
116 3 115 syl5 ⊢ A ∈ Word V ∧ B ∈ Word V → x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ Word S → A ∈ Word S ∧ B ∈ Word S
117 2 116 sylbid ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word S → A ∈ Word S ∧ B ∈ Word S
118 ccatcl ⊢ A ∈ Word S ∧ B ∈ Word S → A ++ B ∈ Word S
119 117 118 impbid1 ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word S ↔ A ∈ Word S ∧ B ∈ Word S