Metamath Proof Explorer

Theorem efgi1

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	efgi1	$⊢ (A \in W \land N \in (0 \dots \|A\|) \land J \in I) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩⟩)$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		1oex	$⊢ 1_{𝑜} \in V$
4	3	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
5		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
6	4 5	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
7	1 2	efgi	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land (J \in I \land 1_{𝑜} \in 2_{𝑜})) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩)$
8	6 7	mpanr2	$⊢ ((A \in W \land N \in (0 \dots \|A\|)) \land J \in I) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩)$
9	8	3impa	$⊢ (A \in W \land N \in (0 \dots \|A\|) \land J \in I) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩)$
10		tru	$⊢ ⊤$
11		eqidd	$⊢ ⊤ \to ⟨J, 1_{𝑜}⟩ = ⟨J, 1_{𝑜}⟩$
12		difid	$⊢ 1_{𝑜} ∖ 1_{𝑜} = \emptyset$
13	12	opeq2i	$⊢ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ = ⟨J, \emptyset⟩$
14	13	a1i	$⊢ ⊤ \to ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ = ⟨J, \emptyset⟩$
15	11 14	s2eqd	$⊢ ⊤ \to ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩ = ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩$
16		oteq3	$⊢ ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩ = ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩ \to ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩⟩$
17	10 15 16	mp2b	$⊢ ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩ = ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩⟩$
18	17	oveq2i	$⊢ A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, 1_{𝑜} ∖ 1_{𝑜}⟩ ”⟩⟩ = A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩⟩$
19	9 18	breqtrdi	$⊢ (A \in W \land N \in (0 \dots \|A\|) \land J \in I) \to A \underset{˙}{\sim} (A splice ⟨N, N, ⟨“ ⟨J, 1_{𝑜}⟩ ⟨J, \emptyset⟩ ”⟩⟩)$