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

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringnegcl.2 ⊢ 𝑋 = ran 𝐺
ringnegcl.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
ringsub.4 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion rngosub ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ringnegcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringnegcl.2 ⊢ 𝑋 = ran 𝐺
3 ringnegcl.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
4 ringsub.4 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
5 1 rngogrpo ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
6 2 3 4 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
7 5 6 syl3an1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )