Theorem efgmval

Description: Value of the formal inverse operation for the generating set of a free group. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Hypothesis	efgmval.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
Assertion	efgmval	$$⊢\left(A\in I\wedge B\in 2_{𝑜}\right)\to AMB=⟨A,1_{𝑜}\setminus B⟩$$

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
2		opeq1	$$⊢a=A\to ⟨a,1_{𝑜}\setminus b⟩=⟨A,1_{𝑜}\setminus b⟩$$
3		difeq2	$$⊢b=B\to 1_{𝑜}\setminus b=1_{𝑜}\setminus B$$
4	3	opeq2d	$$⊢b=B\to ⟨A,1_{𝑜}\setminus b⟩=⟨A,1_{𝑜}\setminus B⟩$$
5		opeq1	$$⊢y=a\to ⟨y,1_{𝑜}\setminus z⟩=⟨a,1_{𝑜}\setminus z⟩$$
6		difeq2	$$⊢z=b\to 1_{𝑜}\setminus z=1_{𝑜}\setminus b$$
7	6	opeq2d	$$⊢z=b\to ⟨a,1_{𝑜}\setminus z⟩=⟨a,1_{𝑜}\setminus b⟩$$
8	5 7	cbvmpov	$$⊢\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)=\left(a\in I,b\in 2_{𝑜}⟼⟨a,1_{𝑜}\setminus b⟩\right)$$
9	1 8	eqtri	$$⊢M=\left(a\in I,b\in 2_{𝑜}⟼⟨a,1_{𝑜}\setminus b⟩\right)$$
10		opex	$$⊢⟨A,1_{𝑜}\setminus B⟩\in \mathrm{V}$$
11	2 4 9 10	ovmpo	$$⊢\left(A\in I\wedge B\in 2_{𝑜}\right)\to AMB=⟨A,1_{𝑜}\setminus B⟩$$