Metamath Proof Explorer


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 = y I , z 2 𝑜 y 1 𝑜 z
Assertion efgmval A I B 2 𝑜 A M B = A 1 𝑜 B

Proof

Step Hyp Ref Expression
1 efgmval.m M = y I , z 2 𝑜 y 1 𝑜 z
2 opeq1 a = A a 1 𝑜 b = A 1 𝑜 b
3 difeq2 b = B 1 𝑜 b = 1 𝑜 B
4 3 opeq2d b = B A 1 𝑜 b = A 1 𝑜 B
5 opeq1 y = a y 1 𝑜 z = a 1 𝑜 z
6 difeq2 z = b 1 𝑜 z = 1 𝑜 b
7 6 opeq2d z = b a 1 𝑜 z = a 1 𝑜 b
8 5 7 cbvmpov y I , z 2 𝑜 y 1 𝑜 z = a I , b 2 𝑜 a 1 𝑜 b
9 1 8 eqtri M = a I , b 2 𝑜 a 1 𝑜 b
10 opex A 1 𝑜 B V
11 2 4 9 10 ovmpo A I B 2 𝑜 A M B = A 1 𝑜 B