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 | |
|
Assertion | efgmval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efgmval.m | |
|
2 | opeq1 | |
|
3 | difeq2 | |
|
4 | 3 | opeq2d | |
5 | opeq1 | |
|
6 | difeq2 | |
|
7 | 6 | opeq2d | |
8 | 5 7 | cbvmpov | |
9 | 1 8 | eqtri | |
10 | opex | |
|
11 | 2 4 9 10 | ovmpo | |