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 e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
Assertion efgmval 
|- ( ( A e. I /\ B e. 2o ) -> ( A M B ) = <. A , ( 1o \ B ) >. )

Proof

Step Hyp Ref Expression
1 efgmval.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
2 opeq1 
 |-  ( a = A -> <. a , ( 1o \ b ) >. = <. A , ( 1o \ b ) >. )
3 difeq2 
 |-  ( b = B -> ( 1o \ b ) = ( 1o \ B ) )
4 3 opeq2d 
 |-  ( b = B -> <. A , ( 1o \ b ) >. = <. A , ( 1o \ B ) >. )
5 opeq1 
 |-  ( y = a -> <. y , ( 1o \ z ) >. = <. a , ( 1o \ z ) >. )
6 difeq2 
 |-  ( z = b -> ( 1o \ z ) = ( 1o \ b ) )
7 6 opeq2d 
 |-  ( z = b -> <. a , ( 1o \ z ) >. = <. a , ( 1o \ b ) >. )
8 5 7 cbvmpov 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( a e. I , b e. 2o |-> <. a , ( 1o \ b ) >. )
9 1 8 eqtri 
 |-  M = ( a e. I , b e. 2o |-> <. a , ( 1o \ b ) >. )
10 opex 
 |-  <. A , ( 1o \ B ) >. e. _V
11 2 4 9 10 ovmpo 
 |-  ( ( A e. I /\ B e. 2o ) -> ( A M B ) = <. A , ( 1o \ B ) >. )