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	sseldi	$⊢ (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	ffvelrni	$⊢ 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	1	fvexi	$⊢ W \in V$
32	31	a1i	$⊢ X \in W \to W \in V$
33		fex2	$⊢ ((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 \land (0 \dots \|X\|) \times (I \times 2_{𝑜}) \in V \land W \in V) \to (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \in V$
34	23 30 32 33	syl3anc	$⊢ X \in W \to (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \in V$
35		fveq2	$⊢ u = X \to \|u\| = \|X\|$
36	35	oveq2d	$⊢ u = X \to (0 \dots \|u\|) = (0 \dots \|X\|)$
37		eqidd	$⊢ u = X \to I \times 2_{𝑜} = I \times 2_{𝑜}$
38		oveq1	$⊢ u = X \to u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
39	36 37 38	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) ”⟩⟩)$
40		oteq1	$⊢ n = a \to ⟨n, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, n, ⟨“ w M (w) ”⟩⟩$
41		oteq2	$⊢ n = a \to ⟨a, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ w M (w) ”⟩⟩$
42	40 41	eqtrd	$⊢ n = a \to ⟨n, n, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ w M (w) ”⟩⟩$
43	42	oveq2d	$⊢ n = a \to v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩ = v splice ⟨a, a, ⟨“ w M (w) ”⟩⟩$
44		id	$⊢ w = b \to w = b$
45		fveq2	$⊢ w = b \to M (w) = M (b)$
46	44 45	s2eqd	$⊢ w = b \to ⟨“ w M (w) ”⟩ = ⟨“ b M (b) ”⟩$
47	46	oteq3d	$⊢ w = b \to ⟨a, a, ⟨“ w M (w) ”⟩⟩ = ⟨a, a, ⟨“ b M (b) ”⟩⟩$
48	47	oveq2d	$⊢ w = b \to v splice ⟨a, a, ⟨“ w M (w) ”⟩⟩ = v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
49	43 48	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) ”⟩⟩)$
50		fveq2	$⊢ v = u \to \|v\| = \|u\|$
51	50	oveq2d	$⊢ v = u \to (0 \dots \|v\|) = (0 \dots \|u\|)$
52		eqidd	$⊢ v = u \to I \times 2_{𝑜} = I \times 2_{𝑜}$
53		oveq1	$⊢ v = u \to v splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
54	51 52 53	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) ”⟩⟩)$
55	49 54	syl5eq	$⊢ 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) ”⟩⟩)$
56	55	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) ”⟩⟩))$
57	4 56	eqtri	$⊢ T = (u \in W ⟼ (a \in (0 \dots \|u\|), b \in (I \times 2_{𝑜}) ⟼ u splice ⟨a, a, ⟨“ b M (b) ”⟩⟩))$
58	39 57	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) ”⟩⟩)$
59	34 58	mpdan	$⊢ X \in W \to T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
60	59	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)$
61	23 60	mpbird	$⊢ X \in W \to T (X) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W$
62	59 61	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