Metamath Proof Explorer

Theorem idl0cl

Description: Obsolete theorem, use ringrng and rng2idl0 instead. An ideal contains 0 . (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	idl0cl.1	$⊢ G = 1^{st} (R)$
		idl0cl.2	$⊢ Z = GId (G)$
	Assertion	idl0cl	$⊢ (R \in RingOps \land I \in Idl (R)) \to Z \in I$

Proof

Step	Hyp	Ref	Expression
1		idl0cl.1	$⊢ G = 1^{st} (R)$
2		idl0cl.2	$⊢ Z = GId (G)$
3		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
4		eqid	$⊢ ran G = ran G$
5	1 3 4 2	isidl	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq ran G \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (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 ran G \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I)))$
7	6	simp2d	$⊢ (R \in RingOps \land I \in Idl (R)) \to Z \in I$