iwrdsplit

Description: Lemma for sseqp1 . (Contributed by Thierry Arnoux, 25-Apr-2019) (Proof shortened by AV, 14-Oct-2022)

	Ref	Expression
Hypotheses	iwrdsplit.s	$⊢ φ \to S \in V$
	iwrdsplit.f	$⊢ φ \to F : ℕ_{0} ⟶ S$
	iwrdsplit.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	iwrdsplit	$⊢ φ \to {F ↾}_{(0 ..^N + 1)} = ({F ↾}_{(0 ..^N)}) ++ ⟨“ F (N) ”⟩$

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	$⊢ φ \to S \in V$
2		iwrdsplit.f	$⊢ φ \to F : ℕ_{0} ⟶ S$
3		iwrdsplit.n	$⊢ φ \to N \in ℕ_{0}$
4		1nn0	$⊢ 1 \in ℕ_{0}$
5	4	a1i	$⊢ φ \to 1 \in ℕ_{0}$
6	3 5	nn0addcld	$⊢ φ \to N + 1 \in ℕ_{0}$
7	1 2 6	subiwrd	$⊢ φ \to {F ↾}_{(0 ..^N + 1)} \in Word S$
8		1re	$⊢ 1 \in ℝ$
9		nn0addge2	$⊢ (1 \in ℝ \land N \in ℕ_{0}) \to 1 \leq N + 1$
10	8 3 9	sylancr	$⊢ φ \to 1 \leq N + 1$
11	1 2 6	subiwrdlen	$⊢ φ \to \|{F ↾}_{(0 ..^N + 1)}\| = N + 1$
12	10 11	breqtrrd	$⊢ φ \to 1 \leq \|{F ↾}_{(0 ..^N + 1)}\|$
13		wrdlenge1n0	$⊢ {F ↾}_{(0 ..^N + 1)} \in Word S \to ({F ↾}_{(0 ..^N + 1)} \neq \emptyset \leftrightarrow 1 \leq \|{F ↾}_{(0 ..^N + 1)}\|)$
14	7 13	syl	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)} \neq \emptyset \leftrightarrow 1 \leq \|{F ↾}_{(0 ..^N + 1)}\|)$
15	12 14	mpbird	$⊢ φ \to {F ↾}_{(0 ..^N + 1)} \neq \emptyset$
16		pfxlswccat	$⊢ ({F ↾}_{(0 ..^N + 1)} \in Word S \land {F ↾}_{(0 ..^N + 1)} \neq \emptyset) \to (({F ↾}_{(0 ..^N + 1)}) prefix (\|{F ↾}_{(0 ..^N + 1)}\| - 1)) ++ ⟨“ lastS ({F ↾}_{(0 ..^N + 1)}) ”⟩ = {F ↾}_{(0 ..^N + 1)}$
17	7 15 16	syl2anc	$⊢ φ \to (({F ↾}_{(0 ..^N + 1)}) prefix (\|{F ↾}_{(0 ..^N + 1)}\| - 1)) ++ ⟨“ lastS ({F ↾}_{(0 ..^N + 1)}) ”⟩ = {F ↾}_{(0 ..^N + 1)}$
18	3	nn0cnd	$⊢ φ \to N \in ℂ$
19		1cnd	$⊢ φ \to 1 \in ℂ$
20	18 19 11	mvrraddd	$⊢ φ \to \|{F ↾}_{(0 ..^N + 1)}\| - 1 = N$
21	20	oveq2d	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)}) prefix (\|{F ↾}_{(0 ..^N + 1)}\| - 1) = ({F ↾}_{(0 ..^N + 1)}) prefix N$
22		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
23	3 22	sylib	$⊢ φ \to N \in (0 \dots N)$
24		elfz0add	$⊢ (N \in ℕ_{0} \land 1 \in ℕ_{0}) \to (N \in (0 \dots N) \to N \in (0 \dots N + 1))$
25	24	imp	$⊢ ((N \in ℕ_{0} \land 1 \in ℕ_{0}) \land N \in (0 \dots N)) \to N \in (0 \dots N + 1)$
26	3 5 23 25	syl21anc	$⊢ φ \to N \in (0 \dots N + 1)$
27	11	oveq2d	$⊢ φ \to (0 \dots \|{F ↾}_{(0 ..^N + 1)}\|) = (0 \dots N + 1)$
28	26 27	eleqtrrd	$⊢ φ \to N \in (0 \dots \|{F ↾}_{(0 ..^N + 1)}\|)$
29		pfxres	$⊢ ({F ↾}_{(0 ..^N + 1)} \in Word S \land N \in (0 \dots \|{F ↾}_{(0 ..^N + 1)}\|)) \to ({F ↾}_{(0 ..^N + 1)}) prefix N = {({F ↾}_{(0 ..^N + 1)}) ↾}_{(0 ..^N)}$
30	7 28 29	syl2anc	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)}) prefix N = {({F ↾}_{(0 ..^N + 1)}) ↾}_{(0 ..^N)}$
31		fzossfzop1	$⊢ N \in ℕ_{0} \to (0 ..^N) \subseteq (0 ..^N + 1)$
32		resabs1	$⊢ (0 ..^N) \subseteq (0 ..^N + 1) \to {({F ↾}_{(0 ..^N + 1)}) ↾}_{(0 ..^N)} = {F ↾}_{(0 ..^N)}$
33	3 31 32	3syl	$⊢ φ \to {({F ↾}_{(0 ..^N + 1)}) ↾}_{(0 ..^N)} = {F ↾}_{(0 ..^N)}$
34	21 30 33	3eqtrd	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)}) prefix (\|{F ↾}_{(0 ..^N + 1)}\| - 1) = {F ↾}_{(0 ..^N)}$
35		lsw	$⊢ {F ↾}_{(0 ..^N + 1)} \in Word S \to lastS ({F ↾}_{(0 ..^N + 1)}) = ({F ↾}_{(0 ..^N + 1)}) (\|{F ↾}_{(0 ..^N + 1)}\| - 1)$
36	7 35	syl	$⊢ φ \to lastS ({F ↾}_{(0 ..^N + 1)}) = ({F ↾}_{(0 ..^N + 1)}) (\|{F ↾}_{(0 ..^N + 1)}\| - 1)$
37	20	fveq2d	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)}) (\|{F ↾}_{(0 ..^N + 1)}\| - 1) = ({F ↾}_{(0 ..^N + 1)}) (N)$
38		fzonn0p1	$⊢ N \in ℕ_{0} \to N \in (0 ..^N + 1)$
39		fvres	$⊢ N \in (0 ..^N + 1) \to ({F ↾}_{(0 ..^N + 1)}) (N) = F (N)$
40	3 38 39	3syl	$⊢ φ \to ({F ↾}_{(0 ..^N + 1)}) (N) = F (N)$
41	36 37 40	3eqtrd	$⊢ φ \to lastS ({F ↾}_{(0 ..^N + 1)}) = F (N)$
42	41	s1eqd	$⊢ φ \to ⟨“ lastS ({F ↾}_{(0 ..^N + 1)}) ”⟩ = ⟨“ F (N) ”⟩$
43	34 42	oveq12d	$⊢ φ \to (({F ↾}_{(0 ..^N + 1)}) prefix (\|{F ↾}_{(0 ..^N + 1)}\| - 1)) ++ ⟨“ lastS ({F ↾}_{(0 ..^N + 1)}) ”⟩ = ({F ↾}_{(0 ..^N)}) ++ ⟨“ F (N) ”⟩$
44	17 43	eqtr3d	$⊢ φ \to {F ↾}_{(0 ..^N + 1)} = ({F ↾}_{(0 ..^N)}) ++ ⟨“ F (N) ”⟩$

Metamath Proof Explorer

Theorem iwrdsplit

Proof