Theorem grpsubid1

Description: Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	grpsubid.b	|- B = ( Base ` G )
	grpsubid.o	|- .0. = ( 0g ` G )
	grpsubid.m	|- .- = ( -g ` G )
Assertion	grpsubid1	|- ( ( G e. Grp /\ X e. B ) -> ( X .- .0. ) = X )

Proof

Step	Hyp	Ref	Expression
1		grpsubid.b	|- B = ( Base ` G )
2		grpsubid.o	|- .0. = ( 0g ` G )
3		grpsubid.m	|- .- = ( -g ` G )
4		id	|- ( X e. B -> X e. B )
5	1 2	grpidcl	|- ( G e. Grp -> .0. e. B )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7		eqid	|- ( invg ` G ) = ( invg ` G )
8	1 6 7 3	grpsubval	|- ( ( X e. B /\ .0. e. B ) -> ( X .- .0. ) = ( X ( +g ` G ) ( ( invg ` G ) ` .0. ) ) )
9	4 5 8	syl2anr	|- ( ( G e. Grp /\ X e. B ) -> ( X .- .0. ) = ( X ( +g ` G ) ( ( invg ` G ) ` .0. ) ) )
10	2 7	grpinvid	|- ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
11	10	adantr	|- ( ( G e. Grp /\ X e. B ) -> ( ( invg ` G ) ` .0. ) = .0. )
12	11	oveq2d	|- ( ( G e. Grp /\ X e. B ) -> ( X ( +g ` G ) ( ( invg ` G ) ` .0. ) ) = ( X ( +g ` G ) .0. ) )
13	1 6 2	grprid	|- ( ( G e. Grp /\ X e. B ) -> ( X ( +g ` G ) .0. ) = X )
14	9 12 13	3eqtrd	|- ( ( G e. Grp /\ X e. B ) -> ( X .- .0. ) = X )