Metamath Proof Explorer

Theorem rngoidl

Description: A ring R is an R ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		rngidl.1	$⊢ G = 1^{st} (R)$
2		rngidl.2	$⊢ X = ran G$
3		ssidd	$⊢ R \in RingOps \to X \subseteq X$
4		eqid	$⊢ GId (G) = GId (G)$
5	1 2 4	rngo0cl	$⊢ R \in RingOps \to GId (G) \in X$
6	1 2	rngogcl	$⊢ (R \in RingOps \land x \in X \land y \in X) \to x G y \in X$
7	6	3expa	$⊢ ((R \in RingOps \land x \in X) \land y \in X) \to x G y \in X$
8	7	ralrimiva	$⊢ (R \in RingOps \land x \in X) \to \forall y \in X x G y \in X$
9		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
10	1 9 2	rngocl	$⊢ (R \in RingOps \land z \in X \land x \in X) \to z 2^{nd} (R) x \in X$
11	10	3com23	$⊢ (R \in RingOps \land x \in X \land z \in X) \to z 2^{nd} (R) x \in X$
12	1 9 2	rngocl	$⊢ (R \in RingOps \land x \in X \land z \in X) \to x 2^{nd} (R) z \in X$
13	11 12	jca	$⊢ (R \in RingOps \land x \in X \land z \in X) \to (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X)$
14	13	3expa	$⊢ ((R \in RingOps \land x \in X) \land z \in X) \to (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X)$
15	14	ralrimiva	$⊢ (R \in RingOps \land x \in X) \to \forall z \in X (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X)$
16	8 15	jca	$⊢ (R \in RingOps \land x \in X) \to (\forall y \in X x G y \in X \land \forall z \in X (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X))$
17	16	ralrimiva	$⊢ R \in RingOps \to \forall x \in X (\forall y \in X x G y \in X \land \forall z \in X (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X))$
18	1 9 2 4	isidl	$⊢ R \in RingOps \to (X \in Idl (R) \leftrightarrow (X \subseteq X \land GId (G) \in X \land \forall x \in X (\forall y \in X x G y \in X \land \forall z \in X (z 2^{nd} (R) x \in X \land x 2^{nd} (R) z \in X))))$
19	3 5 17 18	mpbir3and	$⊢ R \in RingOps \to X \in Idl (R)$