Theorem lidl0

Description: Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lidl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
4		rlm0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
5	2 4	eqtri	⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
6		eqid	⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
7	5 6	lsssn0	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → { 0 } ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
8	3 7	syl	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
9		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10	1 9	eqtri	⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11	8 10	eleqtrrdi	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )