lidl0cl

Description: An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidlcl.u	$⊢ U = LIdeal (R)$
	lidl0cl.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lidl0cl	$⊢ (R \in Ring \land I \in U) \to \underset{˙}{0} \in I$

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		lidl0cl.z	$⊢ \underset{˙}{0} = 0_{R}$
3		rlm0	$⊢ 0_{R} = 0_{ringLMod (R)}$
4	2 3	eqtri	$⊢ \underset{˙}{0} = 0_{ringLMod (R)}$
5		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
6		simpr	$⊢ (R \in Ring \land I \in U) \to I \in U$
7		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
8	1 7	eqtri	$⊢ U = LSubSp (ringLMod (R))$
9	6 8	eleqtrdi	$⊢ (R \in Ring \land I \in U) \to I \in LSubSp (ringLMod (R))$
10		eqid	$⊢ 0_{ringLMod (R)} = 0_{ringLMod (R)}$
11		eqid	$⊢ LSubSp (ringLMod (R)) = LSubSp (ringLMod (R))$
12	10 11	lss0cl	$⊢ (ringLMod (R) \in LMod \land I \in LSubSp (ringLMod (R))) \to 0_{ringLMod (R)} \in I$
13	5 9 12	syl2an2r	$⊢ (R \in Ring \land I \in U) \to 0_{ringLMod (R)} \in I$
14	4 13	eqeltrid	$⊢ (R \in Ring \land I \in U) \to \underset{˙}{0} \in I$

Metamath Proof Explorer