This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lidl1ALT

Description: Alternate proof for lidl1 not using rnglidl1 : Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		rnglidl1.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 → 𝐵 ∈ 𝑈 )