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 )