repswrevw

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

		Ref	Expression
	Assertion	repswrevw	$⊢ (S \in V \land N \in ℕ_{0}) \to reverse (S repeatS N) = S repeatS N$

Proof

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

Metamath Proof Explorer

Theorem repswrevw

Proof