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	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
Assertion	efgmval	⊢ ( ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 2o ) → ( 𝐴 𝑀 𝐵 ) = ⟨ 𝐴 , ( 1o ∖ 𝐵 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
2		opeq1	⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ = ⟨ 𝐴 , ( 1o ∖ 𝑏 ) ⟩ )
3		difeq2	⊢ ( 𝑏 = 𝐵 → ( 1o ∖ 𝑏 ) = ( 1o ∖ 𝐵 ) )
4	3	opeq2d	⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , ( 1o ∖ 𝑏 ) ⟩ = ⟨ 𝐴 , ( 1o ∖ 𝐵 ) ⟩ )
5		opeq1	⊢ ( 𝑦 = 𝑎 → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ = ⟨ 𝑎 , ( 1o ∖ 𝑧 ) ⟩ )
6		difeq2	⊢ ( 𝑧 = 𝑏 → ( 1o ∖ 𝑧 ) = ( 1o ∖ 𝑏 ) )
7	6	opeq2d	⊢ ( 𝑧 = 𝑏 → ⟨ 𝑎 , ( 1o ∖ 𝑧 ) ⟩ = ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
8	5 7	cbvmpov	⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) = ( 𝑎 ∈ 𝐼 , 𝑏 ∈ 2o ↦ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
9	1 8	eqtri	⊢ 𝑀 = ( 𝑎 ∈ 𝐼 , 𝑏 ∈ 2o ↦ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
10		opex	⊢ ⟨ 𝐴 , ( 1o ∖ 𝐵 ) ⟩ ∈ V
11	2 4 9 10	ovmpo	⊢ ( ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 2o ) → ( 𝐴 𝑀 𝐵 ) = ⟨ 𝐴 , ( 1o ∖ 𝐵 ) ⟩ )