Metamath Proof Explorer

Theorem rhmimasubrng

Description: The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025)

Ref Expression
Assertion rhmimasubrng ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRng ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rhmghm ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
2 subrngsubg ⊢ ( 𝑋 ∈ ( SubRng ‘ 𝑀 ) → 𝑋 ∈ ( SubGrp ‘ 𝑀 ) )
3 ghmima ⊢ ( ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
5 eqid ⊢ ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 )
6 eqid ⊢ ( mulGrp ‘ 𝑁 ) = ( mulGrp ‘ 𝑁 )
7 5 6 rhmmhm ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) )
8 simpl ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) )
9 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
10 5 9 mgpbas ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( mulGrp ‘ 𝑀 ) )
11 10 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ 𝑀 ) ) = ( Base ‘ 𝑀 )
12 11 subrngss ⊢ ( 𝑋 ∈ ( SubRng ‘ 𝑀 ) → 𝑋 ⊆ ( Base ‘ ( mulGrp ‘ 𝑀 ) ) )
13 12 adantl ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → 𝑋 ⊆ ( Base ‘ ( mulGrp ‘ 𝑀 ) ) )
14 eqidd ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( +g ‘ ( mulGrp ‘ 𝑀 ) ) = ( +g ‘ ( mulGrp ‘ 𝑀 ) ) )
15 eqidd ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( +g ‘ ( mulGrp ‘ 𝑁 ) ) = ( +g ‘ ( mulGrp ‘ 𝑁 ) ) )
16 eqid ⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
17 5 16 mgpplusg ⊢ ( .r ‘ 𝑀 ) = ( +g ‘ ( mulGrp ‘ 𝑀 ) )
18 17 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑀 ) ) = ( .r ‘ 𝑀 )
19 18 subrngmcl ⊢ ( ( 𝑋 ∈ ( SubRng ‘ 𝑀 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ ( mulGrp ‘ 𝑀 ) ) 𝑥 ) ∈ 𝑋 )
20 19 3adant1l ⊢ ( ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ ( mulGrp ‘ 𝑀 ) ) 𝑥 ) ∈ 𝑋 )
21 8 13 14 15 20 mhmimalem ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑁 ) ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
22 eqid ⊢ ( .r ‘ 𝑁 ) = ( .r ‘ 𝑁 )
23 6 22 mgpplusg ⊢ ( .r ‘ 𝑁 ) = ( +g ‘ ( mulGrp ‘ 𝑁 ) )
24 23 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑁 ) ) = ( .r ‘ 𝑁 )
25 24 oveqi ⊢ ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑁 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 )
26 25 eleq1i ⊢ ( ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑁 ) ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
27 26 2ralbii ⊢ ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑁 ) ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
28 21 27 sylib ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
29 7 28 sylan ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
30 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑁 ∈ Ring )
31 ringrng ⊢ ( 𝑁 ∈ Ring → 𝑁 ∈ Rng )
32 30 31 syl ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑁 ∈ Rng )
33 32 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → 𝑁 ∈ Rng )
34 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
35 34 22 issubrng2 ⊢ ( 𝑁 ∈ Rng → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRng ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
36 33 35 syl ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRng ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( .r ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
37 4 29 36 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRng ‘ 𝑁 ) )