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		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
4		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
5	3 4	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
6	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)$$
7	5 6	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)$$
8	7	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)$$
9		tru	$$⊢\top$$
10		eqidd	$$⊢\top \to ⟨J,1_{𝑜}⟩=⟨J,1_{𝑜}⟩$$
11		difid	$$⊢1_{𝑜}\setminus 1_{𝑜}=\varnothing$$
12	11	opeq2i	$$⊢⟨J,1_{𝑜}\setminus 1_{𝑜}⟩=⟨J,\varnothing ⟩$$
13	12	a1i	$$⊢\top \to ⟨J,1_{𝑜}\setminus 1_{𝑜}⟩=⟨J,\varnothing ⟩$$
14	10 13	s2eqd	$$⊢\top \to ⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩=⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩$$
15		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 ⟩”⟩⟩$$
16	9 14 15	mp2b	$$⊢⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩=⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩$$
17	16	oveq2i	$$⊢A\mathrm{splice}⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,1_{𝑜}\setminus 1_{𝑜}⟩”⟩⟩=A\mathrm{splice}⟨N,N,⟨“⟨J,1_{𝑜}⟩⟨J,\varnothing ⟩”⟩⟩$$
18	8 17	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)$$