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=\mathrm{2Ideal}\left(R\right)$$
	ker2idl.0	$$⊢\underset{\dot{}}{0}=0_S$$
Assertion	ker2idl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in I$$

Proof

Step	Hyp	Ref	Expression
1		ker2idl.i	$$⊢I=\mathrm{2Ideal}\left(R\right)$$
2		ker2idl.0	$$⊢\underset{\dot{}}{0}=0_S$$
3		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
4	3 2	kerlidl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left(R\right)$$
5		rhmopp	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left({opp}_r\left(R\right)\mathrm{RingHom}{opp}_r\left(S\right)\right)$$
6		eqid	$$⊢\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)=\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
7		eqid	$$⊢{opp}_r\left(S\right)={opp}_r\left(S\right)$$
8	7 2	oppr0	$$⊢\underset{\dot{}}{0}=0_{{opp}_r\left(S\right)}$$
9	6 8	kerlidl	$$⊢F\in \left({opp}_r\left(R\right)\mathrm{RingHom}{opp}_r\left(S\right)\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
10	5 9	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
11		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
12	3 11 6 1	2idlelb	$$⊢F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in I\leftrightarrow \left(F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left(R\right)\wedge F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)\right)$$
13	4 10 12	sylanbrc	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in I$$