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

Metamath Proof Explorer

Theorem rngorcan

Description: Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ringgcl.1 ⊢ G = 1 st ⁡ R
ringgcl.2 ⊢ X = ran ⁡ G
Assertion rngorcan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B

Proof

Step Hyp Ref Expression
1 ringgcl.1 ⊢ G = 1 st ⁡ R
2 ringgcl.2 ⊢ X = ran ⁡ G
3 1 rngogrpo ⊢ R ∈ RingOps → G ∈ GrpOp
4 2 grporcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B
5 3 4 sylan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B