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

Metamath Proof Explorer

Theorem lidl0ALT

Description: Alternate proof for lidl0 not using rnglidl0 : Every ring contains a zero 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)$
		rnglidl0.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	lidl0ALT	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in U$

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	$⊢ U = LIdeal (R)$
2		rnglidl0.z	$⊢ \underset{˙}{0} = 0_{R}$
3		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
4		rlm0	$⊢ 0_{R} = 0_{ringLMod (R)}$
5	2 4	eqtri	$⊢ \underset{˙}{0} = 0_{ringLMod (R)}$
6		eqid	$⊢ LSubSp (ringLMod (R)) = LSubSp (ringLMod (R))$
7	5 6	lsssn0	$⊢ ringLMod (R) \in LMod \to \{\underset{˙}{0}\} \in LSubSp (ringLMod (R))$
8	3 7	syl	$⊢ R \in Ring \to \{\underset{˙}{0}\} \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 \{\underset{˙}{0}\} \in U$