rngo1cl

Description: The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ring1cl.1	$⊢ X = ran 1^{st} (R)$
	ring1cl.2	$⊢ H = 2^{nd} (R)$
	ring1cl.3	$⊢ U = GId (H)$
Assertion	rngo1cl	$⊢ R \in RingOps \to U \in X$

Proof

Step	Hyp	Ref	Expression
1		ring1cl.1	$⊢ X = ran 1^{st} (R)$
2		ring1cl.2	$⊢ H = 2^{nd} (R)$
3		ring1cl.3	$⊢ U = GId (H)$
4	2	rngomndo	$⊢ R \in RingOps \to H \in MndOp$
5	2	eleq1i	$⊢ H \in MndOp \leftrightarrow 2^{nd} (R) \in MndOp$
6		mndoismgmOLD	$⊢ 2^{nd} (R) \in MndOp \to 2^{nd} (R) \in Magma$
7		mndoisexid	$⊢ 2^{nd} (R) \in MndOp \to 2^{nd} (R) \in ExId$
8	6 7	jca	$⊢ 2^{nd} (R) \in MndOp \to (2^{nd} (R) \in Magma \land 2^{nd} (R) \in ExId)$
9	5 8	sylbi	$⊢ H \in MndOp \to (2^{nd} (R) \in Magma \land 2^{nd} (R) \in ExId)$
10	4 9	syl	$⊢ R \in RingOps \to (2^{nd} (R) \in Magma \land 2^{nd} (R) \in ExId)$
11		elin	$⊢ 2^{nd} (R) \in (Magma \cap ExId) \leftrightarrow (2^{nd} (R) \in Magma \land 2^{nd} (R) \in ExId)$
12	10 11	sylibr	$⊢ R \in RingOps \to 2^{nd} (R) \in (Magma \cap ExId)$
13		eqid	$⊢ ran 2^{nd} (R) = ran 2^{nd} (R)$
14	2	fveq2i	$⊢ GId (H) = GId (2^{nd} (R))$
15	3 14	eqtri	$⊢ U = GId (2^{nd} (R))$
16	13 15	iorlid	$⊢ 2^{nd} (R) \in (Magma \cap ExId) \to U \in ran 2^{nd} (R)$
17	12 16	syl	$⊢ R \in RingOps \to U \in ran 2^{nd} (R)$
18		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
19		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
20	18 19	rngorn1eq	$⊢ R \in RingOps \to ran 1^{st} (R) = ran 2^{nd} (R)$
21		eqtr	$⊢ (X = ran 1^{st} (R) \land ran 1^{st} (R) = ran 2^{nd} (R)) \to X = ran 2^{nd} (R)$
22	21	eleq2d	$⊢ (X = ran 1^{st} (R) \land ran 1^{st} (R) = ran 2^{nd} (R)) \to (U \in X \leftrightarrow U \in ran 2^{nd} (R))$
23	1 20 22	sylancr	$⊢ R \in RingOps \to (U \in X \leftrightarrow U \in ran 2^{nd} (R))$
24	17 23	mpbird	$⊢ R \in RingOps \to U \in X$

Metamath Proof Explorer

Theorem rngo1cl

Proof