This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpsubf

Description: Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses grpsubcl.b 
|- B = ( Base ` G )
grpsubcl.m 
|- .- = ( -g ` G )
Assertion grpsubf 
|- ( G e. Grp -> .- : ( B X. B ) --> B )

Proof

Step Hyp Ref Expression
1 grpsubcl.b 
 |-  B = ( Base ` G )
2 grpsubcl.m 
 |-  .- = ( -g ` G )
3 eqid 
 |-  ( invg ` G ) = ( invg ` G )
4 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
5 4 3adant2 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 1 6 grpcl 
 |-  ( ( G e. Grp /\ x e. B /\ ( ( invg ` G ) ` y ) e. B ) -> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. B )
8 5 7 syld3an3 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. B )
9 8 3expb 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. B )
10 9 ralrimivva 
 |-  ( G e. Grp -> A. x e. B A. y e. B ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. B )
11 1 6 3 2 grpsubfval 
 |-  .- = ( x e. B , y e. B |-> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) )
12 11 fmpo 
 |-  ( A. x e. B A. y e. B ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) e. B <-> .- : ( B X. B ) --> B )
13 10 12 sylib 
 |-  ( G e. Grp -> .- : ( B X. B ) --> B )