Metamath Proof Explorer


Theorem rngolcan

Description: Left 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=1stR
ringgcl.2 X=ranG
Assertion rngolcan RRingOpsAXBXCXCGA=CGBA=B

Proof

Step Hyp Ref Expression
1 ringgcl.1 G=1stR
2 ringgcl.2 X=ranG
3 1 rngogrpo RRingOpsGGrpOp
4 2 grpolcan GGrpOpAXBXCXCGA=CGBA=B
5 3 4 sylan RRingOpsAXBXCXCGA=CGBA=B