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 ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 repeatS 𝑁 ) ++ ( 𝑆 repeatS 𝑀 ) ) = ( 𝑆 repeatS ( 𝑁 + 𝑀 ) ) )

Proof

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