Metamath Proof Explorer

Theorem rngohomsub

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

Ref Expression
Hypotheses rnghomsub.1 ⊢ G = 1 st ⁡ R
rnghomsub.2 ⊢ X = ran ⁡ G
rnghomsub.3 ⊢ H = / g ⁡ G
rnghomsub.4 ⊢ J = 1 st ⁡ S
rnghomsub.5 ⊢ K = / g ⁡ J
Assertion rngohomsub ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S ∧ A ∈ X ∧ B ∈ X → F ⁡ A H B = F ⁡ A K F ⁡ B

Proof

Step Hyp Ref Expression
1 rnghomsub.1 ⊢ G = 1 st ⁡ R
2 rnghomsub.2 ⊢ X = ran ⁡ G
3 rnghomsub.3 ⊢ H = / g ⁡ G
4 rnghomsub.4 ⊢ J = 1 st ⁡ S
5 rnghomsub.5 ⊢ K = / g ⁡ J
6 1 rngogrpo ⊢ R ∈ RingOps → G ∈ GrpOp
7 6 3ad2ant1 ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → G ∈ GrpOp
8 4 rngogrpo ⊢ S ∈ RingOps → J ∈ GrpOp
9 8 3ad2ant2 ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → J ∈ GrpOp
10 1 4 rngogrphom ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F ∈ G GrpOpHom J
11 7 9 10 3jca ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → G ∈ GrpOp ∧ J ∈ GrpOp ∧ F ∈ G GrpOpHom J
12 2 3 5 ghomdiv ⊢ G ∈ GrpOp ∧ J ∈ GrpOp ∧ F ∈ G GrpOpHom J ∧ A ∈ X ∧ B ∈ X → F ⁡ A H B = F ⁡ A K F ⁡ B
13 11 12 sylan ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S ∧ A ∈ X ∧ B ∈ X → F ⁡ A H B = F ⁡ A K F ⁡ B