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	$⊢ U = LIdeal (R)$
		rnglidl1.b	$⊢ B = {Base}_{R}$
	Assertion	lidl1ALT	$⊢ R \in Ring \to B \in U$

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	$⊢ U = LIdeal (R)$
2		rnglidl1.b	$⊢ B = {Base}_{R}$
3		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
4		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
5	2 4	eqtri	$⊢ B = {Base}_{ringLMod (R)}$
6		eqid	$⊢ LSubSp (ringLMod (R)) = LSubSp (ringLMod (R))$
7	5 6	lss1	$⊢ ringLMod (R) \in LMod \to B \in LSubSp (ringLMod (R))$
8	3 7	syl	$⊢ R \in Ring \to B \in LSubSp (ringLMod (R))$
9		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
10	1 9	eqtri	$⊢ U = LSubSp (ringLMod (R))$
11	8 10	eleqtrrdi	$⊢ R \in Ring \to B \in U$