Metamath Proof Explorer

Theorem grpsubpropd

Description: Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015)

Ref Expression
Hypotheses grpsubpropd.b 
|- ( ph -> ( Base ` G ) = ( Base ` H ) )
grpsubpropd.p 
|- ( ph -> ( +g ` G ) = ( +g ` H ) )
Assertion grpsubpropd 
|- ( ph -> ( -g ` G ) = ( -g ` H ) )

Proof

Step Hyp Ref Expression
1 grpsubpropd.b 
 |-  ( ph -> ( Base ` G ) = ( Base ` H ) )
2 grpsubpropd.p 
 |-  ( ph -> ( +g ` G ) = ( +g ` H ) )
3 eqidd 
 |-  ( ph -> a = a )
4 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
5 2 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
6 4 1 5 grpinvpropd 
 |-  ( ph -> ( invg ` G ) = ( invg ` H ) )
7 6 fveq1d 
 |-  ( ph -> ( ( invg ` G ) ` b ) = ( ( invg ` H ) ` b ) )
8 2 3 7 oveq123d 
 |-  ( ph -> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
9 1 1 8 mpoeq123dv 
 |-  ( ph -> ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) ) = ( a e. ( Base ` H ) , b e. ( Base ` H ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 eqid 
 |-  ( +g ` G ) = ( +g ` G )
12 eqid 
 |-  ( invg ` G ) = ( invg ` G )
13 eqid 
 |-  ( -g ` G ) = ( -g ` G )
14 10 11 12 13 grpsubfval 
 |-  ( -g ` G ) = ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) )
15 eqid 
 |-  ( Base ` H ) = ( Base ` H )
16 eqid 
 |-  ( +g ` H ) = ( +g ` H )
17 eqid 
 |-  ( invg ` H ) = ( invg ` H )
18 eqid 
 |-  ( -g ` H ) = ( -g ` H )
19 15 16 17 18 grpsubfval 
 |-  ( -g ` H ) = ( a e. ( Base ` H ) , b e. ( Base ` H ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
20 9 14 19 3eqtr4g 
 |-  ( ph -> ( -g ` G ) = ( -g ` H ) )