Metamath Proof Explorer

Theorem idlss

Description: Obsolete theorem, use 2idlss instead. An ideal of R is a subset of R . (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	idlss.1	$⊢ G = 1^{st} (R)$
		idlss.2	$⊢ X = ran G$
	Assertion	idlss	$⊢ (R \in RingOps \land I \in Idl (R)) \to I \subseteq X$

Proof

Step	Hyp	Ref	Expression
1		idlss.1	$⊢ G = 1^{st} (R)$
2		idlss.2	$⊢ X = ran G$
3		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
4		eqid	$⊢ GId (G) = GId (G)$
5	1 3 2 4	isidl	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land GId (G) \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I))))$
6	5	biimpa	$⊢ (R \in RingOps \land I \in Idl (R)) \to (I \subseteq X \land GId (G) \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I)))$
7	6	simp1d	$⊢ (R \in RingOps \land I \in Idl (R)) \to I \subseteq X$