Theorem ker2idl

Description: The kernel of a ring homomorphism is a two-sided ideal. (Contributed by Jeff Madsen, 3-Jan-2011) (Revised by AV, 24-Aug-2026)

	Ref	Expression
Hypotheses	ker2idl.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
	ker2idl.0	⊢ 0 = ( 0g ‘ 𝑆 )
Assertion	ker2idl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ker2idl.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
2		ker2idl.0	⊢ 0 = ( 0g ‘ 𝑆 )
3		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4	3 2	kerlidl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LIdeal ‘ 𝑅 ) )
5		rhmopp	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( oppr ‘ 𝑅 ) RingHom ( oppr ‘ 𝑆 ) ) )
6		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
7		eqid	⊢ ( oppr ‘ 𝑆 ) = ( oppr ‘ 𝑆 )
8	7 2	oppr0	⊢ 0 = ( 0g ‘ ( oppr ‘ 𝑆 ) )
9	6 8	kerlidl	⊢ ( 𝐹 ∈ ( ( oppr ‘ 𝑅 ) RingHom ( oppr ‘ 𝑆 ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
10	5 9	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
11		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
12	3 11 6 1	2idlelb	⊢ ( ( ◡ 𝐹 “ { 0 } ) ∈ 𝐼 ↔ ( ( ◡ 𝐹 “ { 0 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ◡ 𝐹 “ { 0 } ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
13	4 10 12	sylanbrc	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝐼 )