Metamath Proof Explorer

Theorem grpsubpropd2

Description: Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses grpsubpropd2.1 
|- ( ph -> B = ( Base ` G ) )
grpsubpropd2.2 
|- ( ph -> B = ( Base ` H ) )
grpsubpropd2.3 
|- ( ph -> G e. Grp )
grpsubpropd2.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
Assertion grpsubpropd2 
|- ( ph -> ( -g ` G ) = ( -g ` H ) )

Proof

Step Hyp Ref Expression
1 grpsubpropd2.1 
 |-  ( ph -> B = ( Base ` G ) )
2 grpsubpropd2.2 
 |-  ( ph -> B = ( Base ` H ) )
3 grpsubpropd2.3 
 |-  ( ph -> G e. Grp )
4 grpsubpropd2.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
5 simp1 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ph )
6 simp2 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> a e. ( Base ` G ) )
7 1 3ad2ant1 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> B = ( Base ` G ) )
8 6 7 eleqtrrd 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> a e. B )
9 3 3ad2ant1 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> G e. Grp )
10 simp3 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> b e. ( Base ` G ) )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 eqid 
 |-  ( invg ` G ) = ( invg ` G )
13 11 12 grpinvcl 
 |-  ( ( G e. Grp /\ b e. ( Base ` G ) ) -> ( ( invg ` G ) ` b ) e. ( Base ` G ) )
14 9 10 13 syl2anc 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( ( invg ` G ) ` b ) e. ( Base ` G ) )
15 14 7 eleqtrrd 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( ( invg ` G ) ` b ) e. B )
16 4 oveqrspc2v 
 |-  ( ( ph /\ ( a e. B /\ ( ( invg ` G ) ` b ) e. B ) ) -> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` G ) ` b ) ) )
17 5 8 15 16 syl12anc 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` G ) ` b ) ) )
18 1 2 4 grpinvpropd 
 |-  ( ph -> ( invg ` G ) = ( invg ` H ) )
19 18 fveq1d 
 |-  ( ph -> ( ( invg ` G ) ` b ) = ( ( invg ` H ) ` b ) )
20 19 oveq2d 
 |-  ( ph -> ( a ( +g ` H ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
21 20 3ad2ant1 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` H ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
22 17 21 eqtrd 
 |-  ( ( ph /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
23 22 mpoeq3dva 
 |-  ( ph -> ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) ) = ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) )
24 1 2 eqtr3d 
 |-  ( ph -> ( Base ` G ) = ( Base ` H ) )
25 mpoeq12 
 |-  ( ( ( Base ` G ) = ( Base ` H ) /\ ( Base ` G ) = ( Base ` H ) ) -> ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) = ( a e. ( Base ` H ) , b e. ( Base ` H ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) )
26 24 24 25 syl2anc 
 |-  ( ph -> ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) = ( a e. ( Base ` H ) , b e. ( Base ` H ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) ) )
27 23 26 eqtrd 
 |-  ( 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 ) ) ) )
28 eqid 
 |-  ( +g ` G ) = ( +g ` G )
29 eqid 
 |-  ( -g ` G ) = ( -g ` G )
30 11 28 12 29 grpsubfval 
 |-  ( -g ` G ) = ( a e. ( Base ` G ) , b e. ( Base ` G ) |-> ( a ( +g ` G ) ( ( invg ` G ) ` b ) ) )
31 eqid 
 |-  ( Base ` H ) = ( Base ` H )
32 eqid 
 |-  ( +g ` H ) = ( +g ` H )
33 eqid 
 |-  ( invg ` H ) = ( invg ` H )
34 eqid 
 |-  ( -g ` H ) = ( -g ` H )
35 31 32 33 34 grpsubfval 
 |-  ( -g ` H ) = ( a e. ( Base ` H ) , b e. ( Base ` H ) |-> ( a ( +g ` H ) ( ( invg ` H ) ` b ) ) )
36 27 30 35 3eqtr4g 
 |-  ( ph -> ( -g ` G ) = ( -g ` H ) )