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	|- I = ( 2Ideal ` R )
	ker2idl.0	|- .0. = ( 0g ` S )
Assertion	ker2idl	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. I )

Proof

Step	Hyp	Ref	Expression
1		ker2idl.i	|- I = ( 2Ideal ` R )
2		ker2idl.0	|- .0. = ( 0g ` S )
3		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
4	3 2	kerlidl	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. ( LIdeal ` R ) )
5		rhmopp	|- ( F e. ( R RingHom S ) -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) )
6		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
7		eqid	|- ( oppR ` S ) = ( oppR ` S )
8	7 2	oppr0	|- .0. = ( 0g ` ( oppR ` S ) )
9	6 8	kerlidl	|- ( F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) -> ( `' F " { .0. } ) e. ( LIdeal ` ( oppR ` R ) ) )
10	5 9	syl	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. ( LIdeal ` ( oppR ` R ) ) )
11		eqid	|- ( oppR ` R ) = ( oppR ` R )
12	3 11 6 1	2idlelb	|- ( ( `' F " { .0. } ) e. I <-> ( ( `' F " { .0. } ) e. ( LIdeal ` R ) /\ ( `' F " { .0. } ) e. ( LIdeal ` ( oppR ` R ) ) ) )
13	4 10 12	sylanbrc	|- ( F e. ( R RingHom S ) -> ( `' F " { .0. } ) e. I )