efgtf

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	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)$

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		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
6	1 5	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
7		simpl	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X \in W$
8	6 7	sselid	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X \in Word (I \times 2_{𝑜})$
9		simprr	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to b \in (I \times 2_{𝑜})$
10	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
11	10	ffvelcdmi	$⊢ b \in (I \times 2_{𝑜}) \to M (b) \in (I \times 2_{𝑜})$
12	11	ad2antll	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to M (b) \in (I \times 2_{𝑜})$
13	9 12	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_{𝑜})$
14		splcl	$⊢ (X \in Word (I \times 2_{𝑜}) \land ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜})) \to X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in Word (I \times 2_{𝑜})$
15	8 13 14	syl2anc	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in Word (I \times 2_{𝑜})$
16	1	efgrcl	$⊢ X \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
17	16	simprd	$⊢ X \in W \to W = Word (I \times 2_{𝑜})$
18	17	adantr	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to W = Word (I \times 2_{𝑜})$
19	15 18	eleqtrrd	$⊢ (X \in W \land (a \in (0 \dots \|X\|) \land b \in (I \times 2_{𝑜}))) \to X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in W$
20	19	ralrimivva	$⊢ X \in W \to \forall a \in (0 \dots \|X\|) \forall b \in (I \times 2_{𝑜}) X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in W$
21		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) ”⟩⟩)$
22	21	fmpo	$⊢ \forall a \in (0 \dots \|X\|) \forall b \in (I \times 2_{𝑜}) X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in W \leftrightarrow (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W$
23	20 22	sylib	$⊢ X \in W \to (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W$
24		ovex	$⊢ (0 \dots \|X\|) \in V$
25	16	simpld	$⊢ X \in W \to I \in V$
26		2on	$⊢ 2_{𝑜} \in On$
27		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
28	25 26 27	sylancl	$⊢ X \in W \to I \times 2_{𝑜} \in V$
29		xpexg	$⊢ ((0 \dots \|X\|) \in V \land I \times 2_{𝑜} \in V) \to (0 \dots \|X\|) \times (I \times 2_{𝑜}) \in V$
30	24 28 29	sylancr	$⊢ X \in W \to (0 \dots \|X\|) \times (I \times 2_{𝑜}) \in V$
31	23 30	fexd	$⊢ X \in W \to (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \in V$
32		fveq2	$⊢ u = X \to \|u\| = \|X\|$
33	32	oveq2d	$⊢ u = X \to (0 \dots \|u\|) = (0 \dots \|X\|)$
34		eqidd	$⊢ u = X \to I \times 2_{𝑜} = I \times 2_{𝑜}$
35		oveq1	$⊢ u = X \to u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
36	33 34 35	mpoeq123dv	$⊢ u = X \to (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
37		oteq1	$⊢ n = a \to ⟨n, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, n, ⟨“ w M (w) ”⟩⟩$
38		oteq2	$⊢ n = a \to ⟨a, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ w M (w) ”⟩⟩$
39	37 38	eqtrd	$⊢ n = a \to ⟨n, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ w M (w) ”⟩⟩$
40	39	oveq2d	$⊢ n = a \to v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩ = v splice ⟨a, a, ⟨“ w M (w) ”⟩⟩$
41		id	$⊢ w = b \to w = b$
42		fveq2	$⊢ w = b \to M (w) = M (b)$
43	41 42	s2eqd	$⊢ w = b \to ⟨“ w M (w) ”⟩ = ⟨“ b M (b) ”⟩$
44	43	oteq3d	$⊢ w = b \to ⟨a, a, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ b M (b) ”⟩⟩$
45	44	oveq2d	$⊢ w = b \to v splice ⟨a, a, ⟨“ w M (w) ”⟩⟩ = v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
46	40 45	cbvmpov	$⊢ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩) = (a \in (0 \dots \|v\|), b \in (I \times 2_{𝑜}) ⟼ v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
47		fveq2	$⊢ v = u \to \|v\| = \|u\|$
48	47	oveq2d	$⊢ v = u \to (0 \dots \|v\|) = (0 \dots \|u\|)$
49		eqidd	$⊢ v = u \to I \times 2_{𝑜} = I \times 2_{𝑜}$
50		oveq1	$⊢ v = u \to v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
51	48 49 50	mpoeq123dv	$⊢ v = u \to (a \in (0 \dots \|v\|), b \in (I \times 2_{𝑜}) ⟼ v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) = (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
52	46 51	eqtrid	$⊢ v = u \to (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩) = (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
53	52	cbvmptv	$⊢ (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩)) = (u \in W ⟼ (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩))$
54	4 53	eqtri	$⊢ T = (u \in W ⟼ (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩))$
55	36 54	fvmptg	$⊢ (X \in W \land (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \in V) \to T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
56	31 55	mpdan	$⊢ X \in W \to T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
57	56	feq1d	$⊢ X \in W \to (T (X) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W \leftrightarrow (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W)$
58	23 57	mpbird	$⊢ X \in W \to T (X) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W$
59	56 58	jca	$⊢ 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)$

Metamath Proof Explorer

Theorem efgtf

Proof