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 = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	Assertion	efgmval	$⊢ (A \in I \land B \in 2_{𝑜}) \to A M B = ⟨A, 1_{𝑜} ∖ B⟩$

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

Metamath Proof Explorer