repswpfx

Description: A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020)

		Ref	Expression
	Assertion	repswpfx	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (S repeatS N) prefix L = S repeatS L$

Proof

Step	Hyp	Ref	Expression
1		repsw	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N \in Word V$
2	1	3adant3	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to S repeatS N \in Word V$
3		repswlen	$⊢ (S \in V \land N \in ℕ_{0}) \to \|S repeatS N\| = N$
4	3	oveq2d	$⊢ (S \in V \land N \in ℕ_{0}) \to (0 \dots \|S repeatS N\|) = (0 \dots N)$
5	4	eleq2d	$⊢ (S \in V \land N \in ℕ_{0}) \to (L \in (0 \dots \|S repeatS N\|) \leftrightarrow L \in (0 \dots N))$
6	5	biimp3ar	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to L \in (0 \dots \|S repeatS N\|)$
7		pfxlen	$⊢ (S repeatS N \in Word V \land L \in (0 \dots \|S repeatS N\|)) \to \|(S repeatS N) prefix L\| = L$
8	2 6 7	syl2anc	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to \|(S repeatS N) prefix L\| = L$
9		elfznn0	$⊢ L \in (0 \dots N) \to L \in ℕ_{0}$
10		repswlen	$⊢ (S \in V \land L \in ℕ_{0}) \to \|S repeatS L\| = L$
11	9 10	sylan2	$⊢ (S \in V \land L \in (0 \dots N)) \to \|S repeatS L\| = L$
12	11	3adant2	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to \|S repeatS L\| = L$
13	8 12	eqtr4d	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to \|(S repeatS N) prefix L\| = \|S repeatS L\|$
14		simpl1	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to S \in V$
15		simpl2	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to N \in ℕ_{0}$
16		elfzuz3	$⊢ L \in (0 \dots N) \to N \in ℤ_{\geq L}$
17	16	3ad2ant3	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to N \in ℤ_{\geq L}$
18	8	fveq2d	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to ℤ_{\geq \|(S repeatS N) prefix L\|} = ℤ_{\geq L}$
19	17 18	eleqtrrd	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to N \in ℤ_{\geq \|(S repeatS N) prefix L\|}$
20		fzoss2	$⊢ N \in ℤ_{\geq \|(S repeatS N) prefix L\|} \to (0 ..^\|(S repeatS N) prefix L\|) \subseteq (0 ..^N)$
21	19 20	syl	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (0 ..^\|(S repeatS N) prefix L\|) \subseteq (0 ..^N)$
22	21	sselda	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to i \in (0 ..^N)$
23		repswsymb	$⊢ (S \in V \land N \in ℕ_{0} \land i \in (0 ..^N)) \to (S repeatS N) (i) = S$
24	14 15 22 23	syl3anc	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to (S repeatS N) (i) = S$
25	2	adantr	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to S repeatS N \in Word V$
26	6	adantr	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to L \in (0 \dots \|S repeatS N\|)$
27	8	oveq2d	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (0 ..^\|(S repeatS N) prefix L\|) = (0 ..^L)$
28	27	eleq2d	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (i \in (0 ..^\|(S repeatS N) prefix L\|) \leftrightarrow i \in (0 ..^L))$
29	28	biimpa	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to i \in (0 ..^L)$
30		pfxfv	$⊢ (S repeatS N \in Word V \land L \in (0 \dots \|S repeatS N\|) \land i \in (0 ..^L)) \to ((S repeatS N) prefix L) (i) = (S repeatS N) (i)$
31	25 26 29 30	syl3anc	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to ((S repeatS N) prefix L) (i) = (S repeatS N) (i)$
32	9	3ad2ant3	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to L \in ℕ_{0}$
33	32	adantr	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to L \in ℕ_{0}$
34		repswsymb	$⊢ (S \in V \land L \in ℕ_{0} \land i \in (0 ..^L)) \to (S repeatS L) (i) = S$
35	14 33 29 34	syl3anc	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to (S repeatS L) (i) = S$
36	24 31 35	3eqtr4d	$⊢ ((S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \land i \in (0 ..^\|(S repeatS N) prefix L\|)) \to ((S repeatS N) prefix L) (i) = (S repeatS L) (i)$
37	36	ralrimiva	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to \forall i \in (0 ..^\|(S repeatS N) prefix L\|) ((S repeatS N) prefix L) (i) = (S repeatS L) (i)$
38		pfxcl	$⊢ S repeatS N \in Word V \to (S repeatS N) prefix L \in Word V$
39	2 38	syl	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (S repeatS N) prefix L \in Word V$
40		repsw	$⊢ (S \in V \land L \in ℕ_{0}) \to S repeatS L \in Word V$
41	9 40	sylan2	$⊢ (S \in V \land L \in (0 \dots N)) \to S repeatS L \in Word V$
42		eqwrd	$⊢ ((S repeatS N) prefix L \in Word V \land S repeatS L \in Word V) \to ((S repeatS N) prefix L = S repeatS L \leftrightarrow (\|(S repeatS N) prefix L\| = \|S repeatS L\| \land \forall i \in (0 ..^\|(S repeatS N) prefix L\|) ((S repeatS N) prefix L) (i) = (S repeatS L) (i)))$
43	39 41 42	3imp3i2an	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to ((S repeatS N) prefix L = S repeatS L \leftrightarrow (\|(S repeatS N) prefix L\| = \|S repeatS L\| \land \forall i \in (0 ..^\|(S repeatS N) prefix L\|) ((S repeatS N) prefix L) (i) = (S repeatS L) (i)))$
44	13 37 43	mpbir2and	$⊢ (S \in V \land N \in ℕ_{0} \land L \in (0 \dots N)) \to (S repeatS N) prefix L = S repeatS L$

Metamath Proof Explorer

Theorem repswpfx

Proof