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=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
	efgval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
Assertion	efgi0	$$⊢\left(A\in W\wedge N\in \left(0\dots \left|A\right|\right)\wedge J\in I\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
2		efgval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
5		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
6	4 5	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
7	1 2	efgi	$$⊢\left(\left(A\in W\wedge N\in \left(0\dots \left|A\right|\right)\right)\wedge \left(J\in I\wedge \varnothing \in 2_{𝑜}\right)\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩\right)$$
8	6 7	mpanr2	$$⊢\left(\left(A\in W\wedge N\in \left(0\dots \left|A\right|\right)\right)\wedge J\in I\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩\right)$$
9	8	3impa	$$⊢\left(A\in W\wedge N\in \left(0\dots \left|A\right|\right)\wedge J\in I\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩\right)$$
10		tru	$$⊢\top$$
11		eqidd	$$⊢\top \to ⟨J,\varnothing ⟩=⟨J,\varnothing ⟩$$
12		dif0	$$⊢1_{𝑜}\setminus \varnothing =1_{𝑜}$$
13	12	opeq2i	$$⊢⟨J,1_{𝑜}\setminus \varnothing ⟩=⟨J,1_{𝑜}⟩$$
14	13	a1i	$$⊢\top \to ⟨J,1_{𝑜}\setminus \varnothing ⟩=⟨J,1_{𝑜}⟩$$
15	11 14	s2eqd	$$⊢\top \to ⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩=⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩$$
16		oteq3	$$⊢⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩=⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩\to ⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩=⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩⟩$$
17	10 15 16	mp2b	$$⊢⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩=⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩⟩$$
18	17	oveq2i	$$⊢A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}\setminus \varnothing ⟩”⟩⟩=A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩⟩$$
19	9 18	breqtrdi	$$⊢\left(A\in W\wedge N\in \left(0\dots \left|A\right|\right)\wedge J\in I\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,\varnothing ⟩⟨J,1_{𝑜}⟩”⟩⟩\right)$$