efgi

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
Assertion	efgi	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩)$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		fveq2	$⊢ u = A \to \|u\| = \|A\|$
4	3	oveq2d	$⊢ u = A \to (0 \dots \|u\|) = (0 \dots \|A\|)$
5		id	$⊢ u = A \to u = A$
6		oveq1	$⊢ u = A \to u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
7	5 6	breq12d	$⊢ u = A \to (u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
8	7	2ralbidv	$⊢ u = A \to (\forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
9	4 8	raleqbidv	$⊢ u = A \to (\forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow \forall i \in (0 \dots \|A\|) \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
10	9	rspcv	$⊢ A \in W \to (\forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \to \forall i \in (0 \dots \|A\|) \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
11		oteq1	$⊢ i = N \to ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = ⟨N, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
12		oteq2	$⊢ i = N \to ⟨N, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
13	11 12	eqtrd	$⊢ i = N \to ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
14	13	oveq2d	$⊢ i = N \to A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩$
15	14	breq2d	$⊢ i = N \to (A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
16	15	2ralbidv	$⊢ i = N \to (\forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
17	16	rspcv	$⊢ N \in (0 \dots \|A\|) \to (\forall i \in (0 \dots \|A\|) \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \to \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
18	10 17	sylan9	$⊢ (A \in W \land N \in (0 \dots \|A\|)) \to (\forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \to \forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
19		opeq1	$⊢ a = J \to ⟨a, b⟩ = ⟨J, b⟩$
20		opeq1	$⊢ a = J \to ⟨a, 1_{𝑜} ∖ b⟩ = ⟨J, 1_{𝑜} ∖ b⟩$
21	19 20	s2eqd	$⊢ a = J \to ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩ = ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩$
22	21	oteq3d	$⊢ a = J \to ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩$
23	22	oveq2d	$⊢ a = J \to A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ = A splice ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩$
24	23	breq2d	$⊢ a = J \to (A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow A r (A splice ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩))$
25		opeq2	$⊢ b = K \to ⟨J, b⟩ = ⟨J, K⟩$
26		difeq2	$⊢ b = K \to 1_{𝑜} ∖ b = 1_{𝑜} ∖ K$
27	26	opeq2d	$⊢ b = K \to ⟨J, 1_{𝑜} ∖ b⟩ = ⟨J, 1_{𝑜} ∖ K⟩$
28	25 27	s2eqd	$⊢ b = K \to ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩ = ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩$
29	28	oteq3d	$⊢ b = K \to ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩$
30	29	oveq2d	$⊢ b = K \to A splice ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩ = A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩$
31	30	breq2d	$⊢ b = K \to (A r (A splice ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow A r (A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩))$
32		df-br	$⊢ A r (A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩) \leftrightarrow ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r$
33	31 32	bitrdi	$⊢ b = K \to (A r (A splice ⟨N, N, ⟨“ ⟨J, b⟩ ⟨J, 1_{𝑜} ∖ b⟩ ”⟩⟩) \leftrightarrow ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
34	24 33	rspc2v	$⊢ (J \in I \land K \in 2_{𝑜}) \to (\forall a \in I \forall b \in 2_{𝑜} A r (A splice ⟨N, N, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
35	18 34	sylan9	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to (\forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
36	35	adantld	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to ((r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
37	36	alrimiv	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to \forall r ((r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
38		opex	$⊢ ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in V$
39	38	elintab	$⊢ ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in ⋂ \{r \| (r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\} \leftrightarrow \forall r ((r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩)) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in r)$
40	37 39	sylibr	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in ⋂ \{r \| (r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\}$
41	1 2	efgval	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall u \in W \forall i \in (0 \dots \|u\|) \forall a \in I \forall b \in 2_{𝑜} u r (u splice ⟨i, i, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩))\}$
42	40 41	eleqtrrdi	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in \underset{˙}{\sim}$
43		df-br	$⊢ A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩) \leftrightarrow ⟨A, A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩⟩ \in \underset{˙}{\sim}$
44	42 43	sylibr	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land K \in 2_{𝑜})) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, K⟩ ⟨J, 1_{𝑜} ∖ K⟩ ”⟩⟩)$

Metamath Proof Explorer

Theorem efgi

Proof