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=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
	efgval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
Assertion	efgi1	$$⊢\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,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩\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		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
4	3	prid2	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
5		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
6	4 5	eleqtrri	$$⊢1_{𝑜}\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 1_{𝑜}\in 2_{𝑜}\right)\right)\to A\underset{\dot{}}{\sim }\left(A\mathrm{splice}⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩\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,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩\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,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩\right)$$
10		tru	$$⊢\top$$
11		eqidd	$$⊢\top \to ⟨J,1_{𝑜}⟩=⟨J,1_{𝑜}⟩$$
12		difid	$$⊢1_{𝑜}\setminus 1_{𝑜}=\varnothing$$
13	12	opeq2i	$$⊢⟨J,1_{𝑜}\setminus 1_{𝑜}⟩=⟨J,\varnothing ⟩$$
14	13	a1i	$$⊢\top \to ⟨J,1_{𝑜}\setminus 1_{𝑜}⟩=⟨J,\varnothing ⟩$$
15	11 14	s2eqd	$$⊢\top \to ⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩=⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩$$
16		oteq3	$$⊢⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩=⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩\to ⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩=⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩$$
17	10 15 16	mp2b	$$⊢⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩=⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩$$
18	17	oveq2i	$$⊢A\mathrm{splice}⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩=A\mathrm{splice}⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩$$
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,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩\right)$$