Theorem rhmima

Description: The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	rhmima	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmghm	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
2		subrgsubg	⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑀 ) → 𝑋 ∈ ( SubGrp ‘ 𝑀 ) )
3		ghmima	⊢ ( ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
5		eqid	⊢ ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 )
6		eqid	⊢ ( mulGrp ‘ 𝑁 ) = ( mulGrp ‘ 𝑁 )
7	5 6	rhmmhm	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) )
8	5	subrgsubm	⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑀 ) → 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑀 ) ) )
9		mhmima	⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑀 ) ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) )
10	7 8 9	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) )
11		rhmrcl2	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑁 ∈ Ring )
12	11	adantr	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → 𝑁 ∈ Ring )
13	6	issubrg3	⊢ ( 𝑁 ∈ Ring → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) ) ) )
14	12 13	syl	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) ) ) )
15	4 10 14	mpbir2and	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) )