Metamath Proof Explorer


Theorem rngohomsub

Description: Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011)

Ref Expression
Hypotheses rnghomsub.1
|- G = ( 1st ` R )
rnghomsub.2
|- X = ran G
rnghomsub.3
|- H = ( /g ` G )
rnghomsub.4
|- J = ( 1st ` S )
rnghomsub.5
|- K = ( /g ` J )
Assertion rngohomsub
|- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 rnghomsub.1
 |-  G = ( 1st ` R )
2 rnghomsub.2
 |-  X = ran G
3 rnghomsub.3
 |-  H = ( /g ` G )
4 rnghomsub.4
 |-  J = ( 1st ` S )
5 rnghomsub.5
 |-  K = ( /g ` J )
6 1 rngogrpo
 |-  ( R e. RingOps -> G e. GrpOp )
7 6 3ad2ant1
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> G e. GrpOp )
8 4 rngogrpo
 |-  ( S e. RingOps -> J e. GrpOp )
9 8 3ad2ant2
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> J e. GrpOp )
10 1 4 rngogrphom
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F e. ( G GrpOpHom J ) )
11 7 9 10 3jca
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( G e. GrpOp /\ J e. GrpOp /\ F e. ( G GrpOpHom J ) ) )
12 2 3 5 ghomdiv
 |-  ( ( ( G e. GrpOp /\ J e. GrpOp /\ F e. ( G GrpOpHom J ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )
13 11 12 sylan
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )