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 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
isrnghmmul.n ⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
Assertion isrnghmmul ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 isrnghmmul.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 isrnghmmul.n ⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
6 3 4 5 isrnghm ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
7 1 rngmgp ⊢ ( 𝑅 ∈ Rng → 𝑀 ∈ Smgrp )
8 sgrpmgm ⊢ ( 𝑀 ∈ Smgrp → 𝑀 ∈ Mgm )
9 7 8 syl ⊢ ( 𝑅 ∈ Rng → 𝑀 ∈ Mgm )
10 2 rngmgp ⊢ ( 𝑆 ∈ Rng → 𝑁 ∈ Smgrp )
11 sgrpmgm ⊢ ( 𝑁 ∈ Smgrp → 𝑁 ∈ Mgm )
12 10 11 syl ⊢ ( 𝑆 ∈ Rng → 𝑁 ∈ Mgm )
13 9 12 anim12i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) )
14 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
15 3 14 ghmf ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
16 13 15 anim12i ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) → ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) )
17 16 biantrurd ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
18 anass ⊢ ( ( ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
19 17 18 bitrdi ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
20 1 3 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
21 2 14 mgpbas ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑁 )
22 1 4 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
23 2 5 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ 𝑁 )
24 20 21 22 23 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ↔ ( ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
25 19 24 bitr4di ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ↔ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) )
26 25 pm5.32da ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) → ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) ) )
27 26 pm5.32i ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) ) )
28 6 27 bitri ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) ) )