Metamath Proof Explorer

Theorem repswrevw

Description: The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018)

Ref Expression
Assertion repswrevw ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( reverse ‘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑆 repeatS 𝑁 ) )

Proof

Step Hyp Ref Expression
1 repswlen ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
2 1 oveq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) = ( 0 ..^ 𝑁 ) )
3 2 mpteq1d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) )
4 simpll ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ 𝑉 )
5 simplr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
6 1 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
7 6 oveq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) = ( 𝑁 − 1 ) )
8 7 oveq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) = ( ( 𝑁 − 1 ) − 𝑥 ) )
9 ubmelm1fzo ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 𝑥 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )
10 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
11 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
12 11 ad2antll ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
13 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
14 13 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑥 ∈ ℂ )
15 1cnd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 1 ∈ ℂ )
16 12 14 15 sub32d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑁 − 𝑥 ) − 1 ) = ( ( 𝑁 − 1 ) − 𝑥 ) )
17 16 eleq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑁 − 𝑥 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) )
18 17 biimpd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑁 − 𝑥 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) )
19 18 ex ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 − 𝑥 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) ) )
20 10 19 syl ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 − 𝑥 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) ) )
21 9 20 mpid ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) )
22 21 impcom ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑁 − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
23 8 22 eqeltrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
24 repswsymb ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) = 𝑆 )
25 4 5 23 24 syl3anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) = 𝑆 )
26 25 mpteq2dva ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
27 3 26 eqtrd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
28 ovex ⊢ ( 𝑆 repeatS 𝑁 ) ∈ V
29 revval ⊢ ( ( 𝑆 repeatS 𝑁 ) ∈ V → ( reverse ‘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) )
30 28 29 mp1i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( reverse ‘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) ) ↦ ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) − 𝑥 ) ) ) )
31 reps ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
32 27 30 31 3eqtr4d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( reverse ‘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑆 repeatS 𝑁 ) )