Theorem kerlidl

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

	Ref	Expression
Hypotheses	kerlidl.i	|- I = ( LIdeal ` R )
	kerlidl.1	|- .0. = ( 0g ` S )
Assertion	kerlidl	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. I )

Proof

Step	Hyp	Ref	Expression
1		kerlidl.i	|- I = ( LIdeal ` R )
2		kerlidl.1	|- .0. = ( 0g ` S )
3		rhmrcl2	|- ( F e. ( R RingHom S ) -> S e. Ring )
4		eqid	|- ( LIdeal ` S ) = ( LIdeal ` S )
5	4 2	lidl0	|- ( S e. Ring -> { .0. } e. ( LIdeal ` S ) )
6	3 5	syl	|- ( F e. ( R RingHom S ) -> { .0. } e. ( LIdeal ` S ) )
7	1	rhmpreimaidl	|- ( ( F e. ( R RingHom S ) /\ { .0. } e. ( LIdeal ` S ) ) -> ( `' F " { .0. } ) e. I )
8	6 7	mpdan	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. I )