efgval2

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	efgval2	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall x \in W ran T (x) \subseteq [x] r)\}$

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	efgval	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall x \in W \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\}$
6	1 2 3 4	efgtf	$⊢ x \in W \to (T (x) = (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \land T (x) : (0 \dots \|x\|) \times (I \times 2_{𝑜}) ⟶ W)$
7	6	simpld	$⊢ x \in W \to T (x) = (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩)$
8	7	rneqd	$⊢ x \in W \to ran T (x) = ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩)$
9	8	sseq1d	$⊢ x \in W \to (ran T (x) \subseteq [x] r \leftrightarrow ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \subseteq [x] r)$
10		dfss3	$⊢ ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \subseteq [x] r \leftrightarrow \forall a \in ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) a \in [x] r$
11		ovex	$⊢ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ \in V$
12	11	rgen2w	$⊢ \forall m \in (0 \dots \|x\|) \forall u \in (I \times 2_{𝑜}) x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ \in V$
13		eqid	$⊢ (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) = (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩)$
14		vex	$⊢ a \in V$
15		vex	$⊢ x \in V$
16	14 15	elec	$⊢ a \in [x] r \leftrightarrow x r a$
17		breq2	$⊢ a = x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ \to (x r a \leftrightarrow x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩))$
18	16 17	syl5bb	$⊢ a = x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ \to (a \in [x] r \leftrightarrow x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩))$
19	13 18	ralrnmpo	$⊢ \forall m \in (0 \dots \|x\|) \forall u \in (I \times 2_{𝑜}) x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ \in V \to (\forall a \in ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) a \in [x] r \leftrightarrow \forall m \in (0 \dots \|x\|) \forall u \in (I \times 2_{𝑜}) x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩))$
20	12 19	ax-mp	$⊢ \forall a \in ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) a \in [x] r \leftrightarrow \forall m \in (0 \dots \|x\|) \forall u \in (I \times 2_{𝑜}) x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩)$
21		id	$⊢ u = ⟨a, b⟩ \to u = ⟨a, b⟩$
22		fveq2	$⊢ u = ⟨a, b⟩ \to M (u) = M (⟨a, b⟩)$
23		df-ov	$⊢ a M b = M (⟨a, b⟩)$
24	22 23	syl6eqr	$⊢ u = ⟨a, b⟩ \to M (u) = a M b$
25	21 24	s2eqd	$⊢ u = ⟨a, b⟩ \to ⟨“ u M (u) ”⟩ = ⟨“ ⟨a, b⟩ (a M b) ”⟩$
26	25	oteq3d	$⊢ u = ⟨a, b⟩ \to ⟨m, m, ⟨“ u M (u) ”⟩⟩ = ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩$
27	26	oveq2d	$⊢ u = ⟨a, b⟩ \to x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩ = x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩$
28	27	breq2d	$⊢ u = ⟨a, b⟩ \to (x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \leftrightarrow x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩))$
29	28	ralxp	$⊢ \forall u \in (I \times 2_{𝑜}) x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \leftrightarrow \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩)$
30		eqidd	$⊢ (a \in I \land b \in 2_{𝑜}) \to ⟨a, b⟩ = ⟨a, b⟩$
31	3	efgmval	$⊢ (a \in I \land b \in 2_{𝑜}) \to a M b = ⟨a, 1_{𝑜} ∖ b⟩$
32	30 31	s2eqd	$⊢ (a \in I \land b \in 2_{𝑜}) \to ⟨“ ⟨a, b⟩ (a M b) ”⟩ = ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩$
33	32	oteq3d	$⊢ (a \in I \land b \in 2_{𝑜}) \to ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩ = ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
34	33	oveq2d	$⊢ (a \in I \land b \in 2_{𝑜}) \to x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩ = x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
35	34	breq2d	$⊢ (a \in I \land b \in 2_{𝑜}) \to (x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩) \leftrightarrow x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
36	35	ralbidva	$⊢ a \in I \to (\forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩) \leftrightarrow \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
37	36	ralbiia	$⊢ \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ (a M b) ”⟩⟩) \leftrightarrow \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
38	29 37	bitri	$⊢ \forall u \in (I \times 2_{𝑜}) x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \leftrightarrow \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
39	38	ralbii	$⊢ \forall m \in (0 \dots \|x\|) \forall u \in (I \times 2_{𝑜}) x r (x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \leftrightarrow \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
40	20 39	bitri	$⊢ \forall a \in ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) a \in [x] r \leftrightarrow \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
41	10 40	bitri	$⊢ ran (m \in (0 \dots \|x\|), u \in (I \times 2_{𝑜}) ⟼ x splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \subseteq [x] r \leftrightarrow \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
42	9 41	syl6bb	$⊢ x \in W \to (ran T (x) \subseteq [x] r \leftrightarrow \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
43	42	ralbiia	$⊢ \forall x \in W ran T (x) \subseteq [x] r \leftrightarrow \forall x \in W \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)$
44	43	anbi2i	$⊢ (r Er W \land \forall x \in W ran T (x) \subseteq [x] r) \leftrightarrow (r Er W \land \forall x \in W \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
45	44	abbii	$⊢ \{r \| (r Er W \land \forall x \in W ran T (x) \subseteq [x] r)\} = \{r \| (r Er W \land \forall x \in W \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\}$
46	45	inteqi	$⊢ ⋂ \{r \| (r Er W \land \forall x \in W ran T (x) \subseteq [x] r)\} = ⋂ \{r \| (r Er W \land \forall x \in W \forall m \in (0 \dots \|x\|) \forall a \in I \forall b \in 2_{𝑜} x r (x splice ⟨m, m, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\}$
47	5 46	eqtr4i	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall x \in W ran T (x) \subseteq [x] r)\}$

Metamath Proof Explorer

Theorem efgval2

Proof