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 ) ) )