efgsp1

Description: If F is an extension sequence and A is an extension of the last element of F , then F + <" A "> is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
Assertion	efgsp1	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F ++ ⟨“ A ”⟩ \in dom S$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7	1 2 3 4 5 6	efgsdm	$⊢ F \in dom S \leftrightarrow (F \in (Word W ∖ \{\emptyset\}) \land F (0) \in D \land \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1)))$
8	7	simp1bi	$⊢ F \in dom S \to F \in (Word W ∖ \{\emptyset\})$
9	8	eldifad	$⊢ F \in dom S \to F \in Word W$
10	1 2 3 4 5 6	efgsf	$⊢ S : \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟶ W$
11	10	fdmi	$⊢ dom S = \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\}$
12	11	feq2i	$⊢ S : dom S ⟶ W \leftrightarrow S : \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟶ W$
13	10 12	mpbir	$⊢ S : dom S ⟶ W$
14	13	ffvelrni	$⊢ F \in dom S \to S (F) \in W$
15	1 2 3 4	efgtf	$⊢ S (F) \in W \to (T (S (F)) = (a \in (0 \dots \|S (F)\|), i \in (I \times 2_{𝑜}) ⟼ S (F) splice ⟨a, a, ⟨“ i M (i) ”⟩⟩) \land T (S (F)) : (0 \dots \|S (F)\|) \times (I \times 2_{𝑜}) ⟶ W)$
16	14 15	syl	$⊢ F \in dom S \to (T (S (F)) = (a \in (0 \dots \|S (F)\|), i \in (I \times 2_{𝑜}) ⟼ S (F) splice ⟨a, a, ⟨“ i M (i) ”⟩⟩) \land T (S (F)) : (0 \dots \|S (F)\|) \times (I \times 2_{𝑜}) ⟶ W)$
17	16	simprd	$⊢ F \in dom S \to T (S (F)) : (0 \dots \|S (F)\|) \times (I \times 2_{𝑜}) ⟶ W$
18	17	frnd	$⊢ F \in dom S \to ran T (S (F)) \subseteq W$
19	18	sselda	$⊢ (F \in dom S \land A \in ran T (S (F))) \to A \in W$
20	19	s1cld	$⊢ (F \in dom S \land A \in ran T (S (F))) \to ⟨“ A ”⟩ \in Word W$
21		ccatcl	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W) \to F ++ ⟨“ A ”⟩ \in Word W$
22	9 20 21	syl2an2r	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F ++ ⟨“ A ”⟩ \in Word W$
23		ccatws1n0	$⊢ F \in Word W \to F ++ ⟨“ A ”⟩ \neq \emptyset$
24	9 23	syl	$⊢ F \in dom S \to F ++ ⟨“ A ”⟩ \neq \emptyset$
25	24	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F ++ ⟨“ A ”⟩ \neq \emptyset$
26		eldifsn	$⊢ F ++ ⟨“ A ”⟩ \in (Word W ∖ \{\emptyset\}) \leftrightarrow (F ++ ⟨“ A ”⟩ \in Word W \land F ++ ⟨“ A ”⟩ \neq \emptyset)$
27	22 25 26	sylanbrc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F ++ ⟨“ A ”⟩ \in (Word W ∖ \{\emptyset\})$
28	9	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F \in Word W$
29		eldifsni	$⊢ F \in (Word W ∖ \{\emptyset\}) \to F \neq \emptyset$
30	8 29	syl	$⊢ F \in dom S \to F \neq \emptyset$
31		len0nnbi	$⊢ F \in Word W \to (F \neq \emptyset \leftrightarrow \|F\| \in ℕ)$
32	9 31	syl	$⊢ F \in dom S \to (F \neq \emptyset \leftrightarrow \|F\| \in ℕ)$
33	30 32	mpbid	$⊢ F \in dom S \to \|F\| \in ℕ$
34		lbfzo0	$⊢ 0 \in (0 ..^\|F\|) \leftrightarrow \|F\| \in ℕ$
35	33 34	sylibr	$⊢ F \in dom S \to 0 \in (0 ..^\|F\|)$
36	35	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to 0 \in (0 ..^\|F\|)$
37		ccatval1	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land 0 \in (0 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (0) = F (0)$
38	28 20 36 37	syl3anc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (0) = F (0)$
39	7	simp2bi	$⊢ F \in dom S \to F (0) \in D$
40	39	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F (0) \in D$
41	38 40	eqeltrd	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (0) \in D$
42	7	simp3bi	$⊢ F \in dom S \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
43	42	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
44		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
45	44	sseli	$⊢ i \in (1 ..^\|F\|) \to i \in (0 ..^\|F\|)$
46		ccatval1	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (0 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (i) = F (i)$
47	45 46	syl3an3	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (1 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (i) = F (i)$
48		elfzoel2	$⊢ i \in (1 ..^\|F\|) \to \|F\| \in ℤ$
49		peano2zm	$⊢ \|F\| \in ℤ \to \|F\| - 1 \in ℤ$
50	48 49	syl	$⊢ i \in (1 ..^\|F\|) \to \|F\| - 1 \in ℤ$
51	48	zred	$⊢ i \in (1 ..^\|F\|) \to \|F\| \in ℝ$
52	51	lem1d	$⊢ i \in (1 ..^\|F\|) \to \|F\| - 1 \leq \|F\|$
53		eluz2	$⊢ \|F\| \in ℤ_{\geq (\|F\| - 1)} \leftrightarrow (\|F\| - 1 \in ℤ \land \|F\| \in ℤ \land \|F\| - 1 \leq \|F\|)$
54	50 48 52 53	syl3anbrc	$⊢ i \in (1 ..^\|F\|) \to \|F\| \in ℤ_{\geq (\|F\| - 1)}$
55		fzoss2	$⊢ \|F\| \in ℤ_{\geq (\|F\| - 1)} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
56	54 55	syl	$⊢ i \in (1 ..^\|F\|) \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
57		elfzo1elm1fzo0	$⊢ i \in (1 ..^\|F\|) \to i - 1 \in (0 ..^\|F\| - 1)$
58	56 57	sseldd	$⊢ i \in (1 ..^\|F\|) \to i - 1 \in (0 ..^\|F\|)$
59		ccatval1	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i - 1 \in (0 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (i - 1) = F (i - 1)$
60	58 59	syl3an3	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (1 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (i - 1) = F (i - 1)$
61	60	fveq2d	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (1 ..^\|F\|)) \to T ((F ++ ⟨“ A ”⟩) (i - 1)) = T (F (i - 1))$
62	61	rneqd	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (1 ..^\|F\|)) \to ran T ((F ++ ⟨“ A ”⟩) (i - 1)) = ran T (F (i - 1))$
63	47 62	eleq12d	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land i \in (1 ..^\|F\|)) \to ((F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow F (i) \in ran T (F (i - 1)))$
64	63	3expa	$⊢ ((F \in Word W \land ⟨“ A ”⟩ \in Word W) \land i \in (1 ..^\|F\|)) \to ((F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow F (i) \in ran T (F (i - 1)))$
65	64	ralbidva	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W) \to (\forall i \in (1 ..^\|F\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1)))$
66	9 20 65	syl2an2r	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (\forall i \in (1 ..^\|F\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1)))$
67	43 66	mpbird	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \forall i \in (1 ..^\|F\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1))$
68		lencl	$⊢ F \in Word W \to \|F\| \in ℕ_{0}$
69	9 68	syl	$⊢ F \in dom S \to \|F\| \in ℕ_{0}$
70	69	nn0cnd	$⊢ F \in dom S \to \|F\| \in ℂ$
71	70	addid2d	$⊢ F \in dom S \to 0 + \|F\| = \|F\|$
72	71	fveq2d	$⊢ F \in dom S \to (F ++ ⟨“ A ”⟩) (0 + \|F\|) = (F ++ ⟨“ A ”⟩) (\|F\|)$
73	72	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (0 + \|F\|) = (F ++ ⟨“ A ”⟩) (\|F\|)$
74		s1len	$⊢ \|⟨“ A ”⟩\| = 1$
75		1nn	$⊢ 1 \in ℕ$
76	74 75	eqeltri	$⊢ \|⟨“ A ”⟩\| \in ℕ$
77		lbfzo0	$⊢ 0 \in (0 ..^\|⟨“ A ”⟩\|) \leftrightarrow \|⟨“ A ”⟩\| \in ℕ$
78	76 77	mpbir	$⊢ 0 \in (0 ..^\|⟨“ A ”⟩\|)$
79	78	a1i	$⊢ (F \in dom S \land A \in ran T (S (F))) \to 0 \in (0 ..^\|⟨“ A ”⟩\|)$
80		ccatval3	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land 0 \in (0 ..^\|⟨“ A ”⟩\|)) \to (F ++ ⟨“ A ”⟩) (0 + \|F\|) = ⟨“ A ”⟩ (0)$
81	28 20 79 80	syl3anc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (0 + \|F\|) = ⟨“ A ”⟩ (0)$
82	73 81	eqtr3d	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (\|F\|) = ⟨“ A ”⟩ (0)$
83		simpr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to A \in ran T (S (F))$
84		s1fv	$⊢ A \in ran T (S (F)) \to ⟨“ A ”⟩ (0) = A$
85	84	adantl	$⊢ (F \in dom S \land A \in ran T (S (F))) \to ⟨“ A ”⟩ (0) = A$
86		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
87	33 86	syl	$⊢ F \in dom S \to \|F\| - 1 \in (0 ..^\|F\|)$
88	87	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \|F\| - 1 \in (0 ..^\|F\|)$
89		ccatval1	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W \land \|F\| - 1 \in (0 ..^\|F\|)) \to (F ++ ⟨“ A ”⟩) (\|F\| - 1) = F (\|F\| - 1)$
90	28 20 88 89	syl3anc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (\|F\| - 1) = F (\|F\| - 1)$
91	1 2 3 4 5 6	efgsval	$⊢ F \in dom S \to S (F) = F (\|F\| - 1)$
92	91	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to S (F) = F (\|F\| - 1)$
93	90 92	eqtr4d	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (\|F\| - 1) = S (F)$
94	93	fveq2d	$⊢ (F \in dom S \land A \in ran T (S (F))) \to T ((F ++ ⟨“ A ”⟩) (\|F\| - 1)) = T (S (F))$
95	94	rneqd	$⊢ (F \in dom S \land A \in ran T (S (F))) \to ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1)) = ran T (S (F))$
96	83 85 95	3eltr4d	$⊢ (F \in dom S \land A \in ran T (S (F))) \to ⟨“ A ”⟩ (0) \in ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1))$
97	82 96	eqeltrd	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (F ++ ⟨“ A ”⟩) (\|F\|) \in ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1))$
98		fvex	$⊢ \|F\| \in V$
99		fveq2	$⊢ i = \|F\| \to (F ++ ⟨“ A ”⟩) (i) = (F ++ ⟨“ A ”⟩) (\|F\|)$
100		fvoveq1	$⊢ i = \|F\| \to (F ++ ⟨“ A ”⟩) (i - 1) = (F ++ ⟨“ A ”⟩) (\|F\| - 1)$
101	100	fveq2d	$⊢ i = \|F\| \to T ((F ++ ⟨“ A ”⟩) (i - 1)) = T ((F ++ ⟨“ A ”⟩) (\|F\| - 1))$
102	101	rneqd	$⊢ i = \|F\| \to ran T ((F ++ ⟨“ A ”⟩) (i - 1)) = ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1))$
103	99 102	eleq12d	$⊢ i = \|F\| \to ((F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow (F ++ ⟨“ A ”⟩) (\|F\|) \in ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1)))$
104	98 103	ralsn	$⊢ \forall i \in \{\|F\|\} (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow (F ++ ⟨“ A ”⟩) (\|F\|) \in ran T ((F ++ ⟨“ A ”⟩) (\|F\| - 1))$
105	97 104	sylibr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \forall i \in \{\|F\|\} (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1))$
106		ralunb	$⊢ \forall i \in ((1 ..^\|F\|) \cup \{\|F\|\}) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow (\forall i \in (1 ..^\|F\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \land \forall i \in \{\|F\|\} (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)))$
107	67 105 106	sylanbrc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \forall i \in ((1 ..^\|F\|) \cup \{\|F\|\}) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1))$
108		ccatlen	$⊢ (F \in Word W \land ⟨“ A ”⟩ \in Word W) \to \|F ++ ⟨“ A ”⟩\| = \|F\| + \|⟨“ A ”⟩\|$
109	9 20 108	syl2an2r	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \|F ++ ⟨“ A ”⟩\| = \|F\| + \|⟨“ A ”⟩\|$
110	74	oveq2i	$⊢ \|F\| + \|⟨“ A ”⟩\| = \|F\| + 1$
111	109 110	eqtrdi	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \|F ++ ⟨“ A ”⟩\| = \|F\| + 1$
112	111	oveq2d	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (1 ..^\|F ++ ⟨“ A ”⟩\|) = (1 ..^\|F\| + 1)$
113		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
114	33 113	eleqtrdi	$⊢ F \in dom S \to \|F\| \in ℤ_{\geq 1}$
115		fzosplitsn	$⊢ \|F\| \in ℤ_{\geq 1} \to (1 ..^\|F\| + 1) = (1 ..^\|F\|) \cup \{\|F\|\}$
116	114 115	syl	$⊢ F \in dom S \to (1 ..^\|F\| + 1) = (1 ..^\|F\|) \cup \{\|F\|\}$
117	116	adantr	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (1 ..^\|F\| + 1) = (1 ..^\|F\|) \cup \{\|F\|\}$
118	112 117	eqtrd	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (1 ..^\|F ++ ⟨“ A ”⟩\|) = (1 ..^\|F\|) \cup \{\|F\|\}$
119	118	raleqdv	$⊢ (F \in dom S \land A \in ran T (S (F))) \to (\forall i \in (1 ..^\|F ++ ⟨“ A ”⟩\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)) \leftrightarrow \forall i \in ((1 ..^\|F\|) \cup \{\|F\|\}) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)))$
120	107 119	mpbird	$⊢ (F \in dom S \land A \in ran T (S (F))) \to \forall i \in (1 ..^\|F ++ ⟨“ A ”⟩\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1))$
121	1 2 3 4 5 6	efgsdm	$⊢ F ++ ⟨“ A ”⟩ \in dom S \leftrightarrow (F ++ ⟨“ A ”⟩ \in (Word W ∖ \{\emptyset\}) \land (F ++ ⟨“ A ”⟩) (0) \in D \land \forall i \in (1 ..^\|F ++ ⟨“ A ”⟩\|) (F ++ ⟨“ A ”⟩) (i) \in ran T ((F ++ ⟨“ A ”⟩) (i - 1)))$
122	27 41 120 121	syl3anbrc	$⊢ (F \in dom S \land A \in ran T (S (F))) \to F ++ ⟨“ A ”⟩ \in dom S$

Metamath Proof Explorer

Theorem efgsp1

Proof