Metamath Proof Explorer

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 = 1^{st} (R)$
	ringnegcl.2	$⊢ X = ran G$
	ringnegcl.3	$⊢ N = inv (G)$
	ringsub.4	$⊢ D = /_{g} (G)$
Assertion	rngosub	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A D B = A G N (B)$

Step	Hyp	Ref	Expression
1		ringnegcl.1	$⊢ G = 1^{st} (R)$
2		ringnegcl.2	$⊢ X = ran G$
3		ringnegcl.3	$⊢ N = inv (G)$
4		ringsub.4	$⊢ D = /_{g} (G)$
5	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
6	2 3 4	grpodivval	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B = A G N (B)$
7	5 6	syl3an1	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A D B = A G N (B)$