Theorem kerlidl

Description: The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		kerlidl.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
2		kerlidl.0	⊢ 0 = ( 0g ‘ 𝑆 )
3		rhmrcl2	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
4		eqid	⊢ ( LIdeal ‘ 𝑆 ) = ( LIdeal ‘ 𝑆 )
5	4 2	lidl0	⊢ ( 𝑆 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑆 ) )
6	3 5	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → { 0 } ∈ ( LIdeal ‘ 𝑆 ) )
7	1	rhmpreimaidl	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ { 0 } ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝐼 )
8	6 7	mpdan	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝐼 )