Theorem lidl1

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

	Ref	Expression
Hypotheses	lidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	lidl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lidl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
4		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
5	2 4	eqtri	⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
6		eqid	⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
7	5 6	lss1	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → 𝐵 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
8	3 7	syl	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
9		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10	1 9	eqtri	⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11	8 10	eleqtrrdi	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )