Metamath Proof Explorer

Theorem isrhm

Description: A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses isrhm.m ⊢ M = mulGrp R
isrhm.n ⊢ N = mulGrp S
Assertion isrhm ⊢ F ∈ R RingHom S ↔ R ∈ Ring ∧ S ∈ Ring ∧ F ∈ R GrpHom S ∧ F ∈ M MndHom N

Proof

Step Hyp Ref Expression
1 isrhm.m ⊢ M = mulGrp R
2 isrhm.n ⊢ N = mulGrp S
3 dfrhm2 ⊢ RingHom = r ∈ Ring , s ∈ Ring ⟼ r GrpHom s ∩ mulGrp r MndHom mulGrp s
4 3 elmpocl ⊢ F ∈ R RingHom S → R ∈ Ring ∧ S ∈ Ring
5 oveq12 ⊢ r = R ∧ s = S → r GrpHom s = R GrpHom S
6 fveq2 ⊢ r = R → mulGrp r = mulGrp R
7 fveq2 ⊢ s = S → mulGrp s = mulGrp S
8 6 7 oveqan12d ⊢ r = R ∧ s = S → mulGrp r MndHom mulGrp s = mulGrp R MndHom mulGrp S
9 5 8 ineq12d ⊢ r = R ∧ s = S → r GrpHom s ∩ mulGrp r MndHom mulGrp s = R GrpHom S ∩ mulGrp R MndHom mulGrp S
10 ovex ⊢ R GrpHom S ∈ V
11 10 inex1 ⊢ R GrpHom S ∩ mulGrp R MndHom mulGrp S ∈ V
12 9 3 11 ovmpoa ⊢ R ∈ Ring ∧ S ∈ Ring → R RingHom S = R GrpHom S ∩ mulGrp R MndHom mulGrp S
13 12 eleq2d ⊢ R ∈ Ring ∧ S ∈ Ring → F ∈ R RingHom S ↔ F ∈ R GrpHom S ∩ mulGrp R MndHom mulGrp S
14 elin ⊢ F ∈ R GrpHom S ∩ mulGrp R MndHom mulGrp S ↔ F ∈ R GrpHom S ∧ F ∈ mulGrp R MndHom mulGrp S
15 1 2 oveq12i ⊢ M MndHom N = mulGrp R MndHom mulGrp S
16 15 eqcomi ⊢ mulGrp R MndHom mulGrp S = M MndHom N
17 16 eleq2i ⊢ F ∈ mulGrp R MndHom mulGrp S ↔ F ∈ M MndHom N
18 17 anbi2i ⊢ F ∈ R GrpHom S ∧ F ∈ mulGrp R MndHom mulGrp S ↔ F ∈ R GrpHom S ∧ F ∈ M MndHom N
19 14 18 bitri ⊢ F ∈ R GrpHom S ∩ mulGrp R MndHom mulGrp S ↔ F ∈ R GrpHom S ∧ F ∈ M MndHom N
20 13 19 bitrdi ⊢ R ∈ Ring ∧ S ∈ Ring → F ∈ R RingHom S ↔ F ∈ R GrpHom S ∧ F ∈ M MndHom N
21 4 20 biadanii ⊢ F ∈ R RingHom S ↔ R ∈ Ring ∧ S ∈ Ring ∧ F ∈ R GrpHom S ∧ F ∈ M MndHom N