Metamath Proof Explorer

Theorem rngogrphom

Description: A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011)

Ref Expression
Hypotheses rnggrphom.1 ⊢ G = 1 st ⁡ R
rnggrphom.2 ⊢ J = 1 st ⁡ S
Assertion rngogrphom ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F ∈ G GrpOpHom J

Proof

Step Hyp Ref Expression
1 rnggrphom.1 ⊢ G = 1 st ⁡ R
2 rnggrphom.2 ⊢ J = 1 st ⁡ S
3 eqid ⊢ ran ⁡ G = ran ⁡ G
4 eqid ⊢ ran ⁡ J = ran ⁡ J
5 1 3 2 4 rngohomf ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F : ran ⁡ G ⟶ ran ⁡ J
6 1 3 2 rngohomadd ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → F ⁡ x G y = F ⁡ x J F ⁡ y
7 6 eqcomd ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → F ⁡ x J F ⁡ y = F ⁡ x G y
8 7 ralrimivva ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x J F ⁡ y = F ⁡ x G y
9 1 rngogrpo ⊢ R ∈ RingOps → G ∈ GrpOp
10 2 rngogrpo ⊢ S ∈ RingOps → J ∈ GrpOp
11 3 4 elghomOLD ⊢ G ∈ GrpOp ∧ J ∈ GrpOp → F ∈ G GrpOpHom J ↔ F : ran ⁡ G ⟶ ran ⁡ J ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x J F ⁡ y = F ⁡ x G y
12 9 10 11 syl2an ⊢ R ∈ RingOps ∧ S ∈ RingOps → F ∈ G GrpOpHom J ↔ F : ran ⁡ G ⟶ ran ⁡ J ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x J F ⁡ y = F ⁡ x G y
13 12 3adant3 ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F ∈ G GrpOpHom J ↔ F : ran ⁡ G ⟶ ran ⁡ J ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x J F ⁡ y = F ⁡ x G y
14 5 8 13 mpbir2and ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F ∈ G GrpOpHom J