Theorem rngosub

Description: Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	ringnegcl.1	|- G = ( 1st ` R )
	ringnegcl.2	|- X = ran G
	ringnegcl.3	|- N = ( inv ` G )
	ringsub.4	|- D = ( /g ` G )
Assertion	rngosub	|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringnegcl.1	|- G = ( 1st ` R )
2		ringnegcl.2	|- X = ran G
3		ringnegcl.3	|- N = ( inv ` G )
4		ringsub.4	|- D = ( /g ` G )
5	1	rngogrpo	|- ( R e. RingOps -> G e. GrpOp )
6	2 3 4	grpodivval	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )
7	5 6	syl3an1	|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )