Theorem lidl0cl

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

	Ref	Expression
Hypotheses	lidlcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidl0cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lidl0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lidl0cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		rlm0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
4	2 3	eqtri	⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
5		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
6		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
7		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
8	1 7	eqtri	⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
9	6 8	eleqtrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
10		eqid	⊢ ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
11		eqid	⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
12	10 11	lss0cl	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) → ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) ∈ 𝐼 )
13	5 9 12	syl2an2r	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) ∈ 𝐼 )
14	4 13	eqeltrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )