Metamath Proof Explorer

Theorem isrnghmmul

Description: A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses isrnghmmul.m ⊢ M = mulGrp R
isrnghmmul.n ⊢ N = mulGrp S
Assertion isrnghmmul ⊢ F ∈ R RngHomo S ↔ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ F ∈ M MgmHom N

Proof

Step Hyp Ref Expression
1 isrnghmmul.m ⊢ M = mulGrp R
2 isrnghmmul.n ⊢ N = mulGrp S
3 eqid ⊢ Base R = Base R
4 eqid ⊢ ⋅ R = ⋅ R
5 eqid ⊢ ⋅ S = ⋅ S
6 3 4 5 isrnghm ⊢ F ∈ R RngHomo S ↔ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y
7 1 rngmgp Could not format ( R e. Rng -> M e. Smgrp ) : No typesetting found for |- ( R e. Rng -> M e. Smgrp ) with typecode |-
8 sgrpmgm Could not format ( M e. Smgrp -> M e. Mgm ) : No typesetting found for |- ( M e. Smgrp -> M e. Mgm ) with typecode |-
9 7 8 syl ⊢ R ∈ Rng → M ∈ Mgm
10 2 rngmgp Could not format ( S e. Rng -> N e. Smgrp ) : No typesetting found for |- ( S e. Rng -> N e. Smgrp ) with typecode |-
11 sgrpmgm Could not format ( N e. Smgrp -> N e. Mgm ) : No typesetting found for |- ( N e. Smgrp -> N e. Mgm ) with typecode |-
12 10 11 syl ⊢ S ∈ Rng → N ∈ Mgm
13 9 12 anim12i ⊢ R ∈ Rng ∧ S ∈ Rng → M ∈ Mgm ∧ N ∈ Mgm
14 eqid ⊢ Base S = Base S
15 3 14 ghmf ⊢ F ∈ R GrpHom S → F : Base R ⟶ Base S
16 13 15 anim12i ⊢ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S → M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S
17 16 biantrurd ⊢ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S → ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y
18 anass ⊢ M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y
19 17 18 bitrdi ⊢ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S → ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y
20 1 3 mgpbas ⊢ Base R = Base M
21 2 14 mgpbas ⊢ Base S = Base N
22 1 4 mgpplusg ⊢ ⋅ R = + M
23 2 5 mgpplusg ⊢ ⋅ S = + N
24 20 21 22 23 ismgmhm ⊢ F ∈ M MgmHom N ↔ M ∈ Mgm ∧ N ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y
25 19 24 bitr4di ⊢ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S → ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ F ∈ M MgmHom N
26 25 pm5.32da ⊢ R ∈ Rng ∧ S ∈ Rng → F ∈ R GrpHom S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ F ∈ R GrpHom S ∧ F ∈ M MgmHom N
27 26 pm5.32i ⊢ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x ⋅ R y = F ⁡ x ⋅ S F ⁡ y ↔ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ F ∈ M MgmHom N
28 6 27 bitri ⊢ F ∈ R RngHomo S ↔ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ F ∈ M MgmHom N