Metamath Proof Explorer

Theorem repswrevw

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

Ref Expression
Assertion repswrevw ⊢S∈V∧N∈ℕ0→reverse⁡SrepeatSN=SrepeatSN

Proof

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