idl0cl

Description: An ideal contains 0 . (Contributed by Jeff Madsen, 10-Jun-2010)

	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$

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$

Metamath Proof Explorer