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=yI,z2𝑜y1𝑜z
Assertion efgmval AIB2𝑜AMB=A1𝑜B

Proof

Step Hyp Ref Expression
1 efgmval.m M=yI,z2𝑜y1𝑜z
2 opeq1 a=Aa1𝑜b=A1𝑜b
3 difeq2 b=B1𝑜b=1𝑜B
4 3 opeq2d b=BA1𝑜b=A1𝑜B
5 opeq1 y=ay1𝑜z=a1𝑜z
6 difeq2 z=b1𝑜z=1𝑜b
7 6 opeq2d z=ba1𝑜z=a1𝑜b
8 5 7 cbvmpov yI,z2𝑜y1𝑜z=aI,b2𝑜a1𝑜b
9 1 8 eqtri M=aI,b2𝑜a1𝑜b
10 opex A1𝑜BV
11 2 4 9 10 ovmpo AIB2𝑜AMB=A1𝑜B