Metamath Proof Explorer

Theorem efgi0

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

Proof

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