Metamath Proof Explorer

Theorem repswccat

Description: The concatenation of two "repeated symbol words" with the same symbol is again a "repeated symbol word". (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repswccat ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N ++ S repeatS M = S repeatS N + M

Proof

Step Hyp Ref Expression
1 repswlen ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N = N
2 1 3adant3 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N = N
3 repswlen ⊢ S ∈ V ∧ M ∈ ℕ 0 → S repeatS M = M
4 3 3adant2 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS M = M
5 2 4 oveq12d ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N + S repeatS M = N + M
6 5 oveq2d ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → 0 ..^ S repeatS N + S repeatS M = 0 ..^ N + M
7 simp1 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S ∈ V
8 7 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N → S ∈ V
9 simpl2 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N → N ∈ ℕ 0
10 2 oveq2d ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → 0 ..^ S repeatS N = 0 ..^ N
11 10 eleq2d ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ S repeatS N ↔ x ∈ 0 ..^ N
12 11 biimpa ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N → x ∈ 0 ..^ N
13 8 9 12 3jca ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N → S ∈ V ∧ N ∈ ℕ 0 ∧ x ∈ 0 ..^ N
14 13 adantlr ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ x ∈ 0 ..^ S repeatS N → S ∈ V ∧ N ∈ ℕ 0 ∧ x ∈ 0 ..^ N
15 repswsymb ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ x ∈ 0 ..^ N → S repeatS N ⁡ x = S
16 14 15 syl ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ x ∈ 0 ..^ S repeatS N → S repeatS N ⁡ x = S
17 7 ad2antrr ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ ¬ x ∈ 0 ..^ S repeatS N → S ∈ V
18 simpll3 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ ¬ x ∈ 0 ..^ S repeatS N → M ∈ ℕ 0
19 2 4 jca ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N = N ∧ S repeatS M = M
20 simpr ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ N + M → x ∈ 0 ..^ N + M
21 20 anim1i ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ N + M ∧ ¬ x ∈ 0 ..^ N → x ∈ 0 ..^ N + M ∧ ¬ x ∈ 0 ..^ N
22 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
23 nn0z ⊢ M ∈ ℕ 0 → M ∈ ℤ
24 22 23 anim12i ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → N ∈ ℤ ∧ M ∈ ℤ
25 24 ad2antrr ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ N + M ∧ ¬ x ∈ 0 ..^ N → N ∈ ℤ ∧ M ∈ ℤ
26 fzocatel ⊢ x ∈ 0 ..^ N + M ∧ ¬ x ∈ 0 ..^ N ∧ N ∈ ℤ ∧ M ∈ ℤ → x − N ∈ 0 ..^ M
27 21 25 26 syl2anc ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ N + M ∧ ¬ x ∈ 0 ..^ N → x − N ∈ 0 ..^ M
28 27 exp31 ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ N + M → ¬ x ∈ 0 ..^ N → x − N ∈ 0 ..^ M
29 28 3adant1 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ N + M → ¬ x ∈ 0 ..^ N → x − N ∈ 0 ..^ M
30 oveq12 ⊢ S repeatS N = N ∧ S repeatS M = M → S repeatS N + S repeatS M = N + M
31 30 oveq2d ⊢ S repeatS N = N ∧ S repeatS M = M → 0 ..^ S repeatS N + S repeatS M = 0 ..^ N + M
32 31 eleq2d ⊢ S repeatS N = N ∧ S repeatS M = M → x ∈ 0 ..^ S repeatS N + S repeatS M ↔ x ∈ 0 ..^ N + M
33 oveq2 ⊢ S repeatS N = N → 0 ..^ S repeatS N = 0 ..^ N
34 33 eleq2d ⊢ S repeatS N = N → x ∈ 0 ..^ S repeatS N ↔ x ∈ 0 ..^ N
35 34 notbid ⊢ S repeatS N = N → ¬ x ∈ 0 ..^ S repeatS N ↔ ¬ x ∈ 0 ..^ N
36 35 adantr ⊢ S repeatS N = N ∧ S repeatS M = M → ¬ x ∈ 0 ..^ S repeatS N ↔ ¬ x ∈ 0 ..^ N
37 oveq2 ⊢ S repeatS N = N → x − S repeatS N = x − N
38 37 eleq1d ⊢ S repeatS N = N → x − S repeatS N ∈ 0 ..^ M ↔ x − N ∈ 0 ..^ M
39 38 adantr ⊢ S repeatS N = N ∧ S repeatS M = M → x − S repeatS N ∈ 0 ..^ M ↔ x − N ∈ 0 ..^ M
40 36 39 imbi12d ⊢ S repeatS N = N ∧ S repeatS M = M → ¬ x ∈ 0 ..^ S repeatS N → x − S repeatS N ∈ 0 ..^ M ↔ ¬ x ∈ 0 ..^ N → x − N ∈ 0 ..^ M
41 32 40 imbi12d ⊢ S repeatS N = N ∧ S repeatS M = M → x ∈ 0 ..^ S repeatS N + S repeatS M → ¬ x ∈ 0 ..^ S repeatS N → x − S repeatS N ∈ 0 ..^ M ↔ x ∈ 0 ..^ N + M → ¬ x ∈ 0 ..^ N → x − N ∈ 0 ..^ M
42 29 41 imbitrrid ⊢ S repeatS N = N ∧ S repeatS M = M → S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ S repeatS N + S repeatS M → ¬ x ∈ 0 ..^ S repeatS N → x − S repeatS N ∈ 0 ..^ M
43 19 42 mpcom ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ S repeatS N + S repeatS M → ¬ x ∈ 0 ..^ S repeatS N → x − S repeatS N ∈ 0 ..^ M
44 43 imp31 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ ¬ x ∈ 0 ..^ S repeatS N → x − S repeatS N ∈ 0 ..^ M
45 repswsymb ⊢ S ∈ V ∧ M ∈ ℕ 0 ∧ x − S repeatS N ∈ 0 ..^ M → S repeatS M ⁡ x − S repeatS N = S
46 17 18 44 45 syl3anc ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M ∧ ¬ x ∈ 0 ..^ S repeatS N → S repeatS M ⁡ x − S repeatS N = S
47 16 46 ifeqda ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ x ∈ 0 ..^ S repeatS N + S repeatS M → if x ∈ 0 ..^ S repeatS N S repeatS N ⁡ x S repeatS M ⁡ x − S repeatS N = S
48 6 47 mpteq12dva ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → x ∈ 0 ..^ S repeatS N + S repeatS M ⟼ if x ∈ 0 ..^ S repeatS N S repeatS N ⁡ x S repeatS M ⁡ x − S repeatS N = x ∈ 0 ..^ N + M ⟼ S
49 ovex ⊢ S repeatS N ∈ V
50 ovex ⊢ S repeatS M ∈ V
51 49 50 pm3.2i ⊢ S repeatS N ∈ V ∧ S repeatS M ∈ V
52 ccatfval ⊢ S repeatS N ∈ V ∧ S repeatS M ∈ V → S repeatS N ++ S repeatS M = x ∈ 0 ..^ S repeatS N + S repeatS M ⟼ if x ∈ 0 ..^ S repeatS N S repeatS N ⁡ x S repeatS M ⁡ x − S repeatS N
53 51 52 mp1i ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N ++ S repeatS M = x ∈ 0 ..^ S repeatS N + S repeatS M ⟼ if x ∈ 0 ..^ S repeatS N S repeatS N ⁡ x S repeatS M ⁡ x − S repeatS N
54 nn0addcl ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → N + M ∈ ℕ 0
55 54 3adant1 ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → N + M ∈ ℕ 0
56 reps ⊢ S ∈ V ∧ N + M ∈ ℕ 0 → S repeatS N + M = x ∈ 0 ..^ N + M ⟼ S
57 7 55 56 syl2anc ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N + M = x ∈ 0 ..^ N + M ⟼ S
58 48 53 57 3eqtr4d ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → S repeatS N ++ S repeatS M = S repeatS N + M