efgtlen

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-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) ”⟩⟩))$
Assertion	efgtlen	$⊢ (X \in W \land A \in ran T (X)) \to \|A\| = \|X\| + 2$

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	1 2 3 4	efgtf	$⊢ X \in W \to (T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (X) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W)$
6	5	simpld	$⊢ X \in W \to T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
7	6	rneqd	$⊢ X \in W \to ran T (X) = ran (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
8	7	eleq2d	$⊢ X \in W \to (A \in ran T (X) \leftrightarrow A \in ran (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩))$
9		eqid	$⊢ (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
10		ovex	$⊢ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in V$
11	9 10	elrnmpo	$⊢ A \in ran (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \leftrightarrow \exists a \in (0 \dots \|X\|) \exists b \in (I \times 2_{𝑜}) A = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
12	8 11	bitrdi	$⊢ X \in W \to (A \in ran T (X) \leftrightarrow \exists a \in (0 \dots \|X\|) \exists b \in (I \times 2_{𝑜}) A = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
13		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
14	1 13	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
15		simpl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X \in W$
16	14 15	sselid	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X \in Word (I \times 2_{𝑜})$
17		elfzuz	$⊢ a \in (0 \dots \|X\|) \to a \in ℤ_{\geq 0}$
18	17	ad2antrl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to a \in ℤ_{\geq 0}$
19		eluzfz2b	$⊢ a \in ℤ_{\geq 0} \leftrightarrow a \in (0 \dots a)$
20	18 19	sylib	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to a \in (0 \dots a)$
21		simprl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to a \in (0 \dots \|X\|)$
22		simprr	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to b \in (I \times 2_{𝑜})$
23	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
24	23	ffvelcdmi	$⊢ b \in (I \times 2_{𝑜}) \to M (b) \in (I \times 2_{𝑜})$
25	22 24	syl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to M (b) \in (I \times 2_{𝑜})$
26	22 25	s2cld	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜})$
27	16 20 21 26	spllen	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩\| = \|X\| + \|⟨“ b M (b) ”⟩\| - (a - a)$
28		s2len	$⊢ \|⟨“ b M (b) ”⟩\| = 2$
29	28	a1i	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|⟨“ b M (b) ”⟩\| = 2$
30		eluzelcn	$⊢ a \in ℤ_{\geq 0} \to a \in ℂ$
31	18 30	syl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to a \in ℂ$
32	31	subidd	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to a - a = 0$
33	29 32	oveq12d	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|⟨“ b M (b) ”⟩\| - (a - a) = 2 - 0$
34		2cn	$⊢ 2 \in ℂ$
35	34	subid1i	$⊢ 2 - 0 = 2$
36	33 35	eqtrdi	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|⟨“ b M (b) ”⟩\| - (a - a) = 2$
37	36	oveq2d	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|X\| + \|⟨“ b M (b) ”⟩\| - (a - a) = \|X\| + 2$
38	27 37	eqtrd	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to \|X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩\| = \|X\| + 2$
39		fveqeq2	$⊢ A = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \to (\|A\| = \|X\| + 2 \leftrightarrow \|X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩\| = \|X\| + 2)$
40	38 39	syl5ibrcom	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to (A = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \to \|A\| = \|X\| + 2)$
41	40	rexlimdvva	$⊢ X \in W \to (\exists a \in (0 \dots \|X\|) \exists b \in (I \times 2_{𝑜}) A = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \to \|A\| = \|X\| + 2)$
42	12 41	sylbid	$⊢ X \in W \to (A \in ran T (X) \to \|A\| = \|X\| + 2)$
43	42	imp	$⊢ (X \in W \land A \in ran T (X)) \to \|A\| = \|X\| + 2$

Metamath Proof Explorer

Theorem efgtlen

Proof