Metamath Proof Explorer

Theorem rhmsub

Description: Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011) (Revised by AV, 10-Jan-2025)

Ref Expression
Hypotheses rhmsub.x 
|- X = ( Base ` R )
rhmsub.m 
|- .- = ( -g ` R )
rhmsub.n 
|- N = ( -g ` S )
Assertion rhmsub 
|- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .- B ) ) = ( ( F ` A ) N ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 rhmsub.x 
 |-  X = ( Base ` R )
2 rhmsub.m 
 |-  .- = ( -g ` R )
3 rhmsub.n 
 |-  N = ( -g ` S )
4 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
5 1 2 3 ghmsub 
 |-  ( ( F e. ( R GrpHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .- B ) ) = ( ( F ` A ) N ( F ` B ) ) )
6 4 5 syl3an1 
 |-  ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .- B ) ) = ( ( F ` A ) N ( F ` B ) ) )