rngoideu

Description: The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	$⊢ G = 1^{st} (R)$
	ringi.2	$⊢ H = 2^{nd} (R)$
	ringi.3	$⊢ X = ran G$
Assertion	rngoideu	$⊢ R \in RingOps \to \exists! u \in X \forall x \in X (u H x = x \land x H u = x)$

Proof

Step	Hyp	Ref	Expression
1		ringi.1	$⊢ G = 1^{st} (R)$
2		ringi.2	$⊢ H = 2^{nd} (R)$
3		ringi.3	$⊢ X = ran G$
4	1 2 3	rngoi	$⊢ R \in RingOps \to ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall u \in X \forall x \in X \forall y \in X ((u H x) H y = u H (x H y) \land u H (x G y) = (u H x) G (u H y) \land (u G x) H y = (u H y) G (x H y)) \land \exists u \in X \forall x \in X (u H x = x \land x H u = x)))$
5	4	simprrd	$⊢ R \in RingOps \to \exists u \in X \forall x \in X (u H x = x \land x H u = x)$
6		simpl	$⊢ (u H x = x \land x H u = x) \to u H x = x$
7	6	ralimi	$⊢ \forall x \in X (u H x = x \land x H u = x) \to \forall x \in X u H x = x$
8		oveq2	$⊢ x = y \to u H x = u H y$
9		id	$⊢ x = y \to x = y$
10	8 9	eqeq12d	$⊢ x = y \to (u H x = x \leftrightarrow u H y = y)$
11	10	rspcv	$⊢ y \in X \to (\forall x \in X u H x = x \to u H y = y)$
12	7 11	syl5	$⊢ y \in X \to (\forall x \in X (u H x = x \land x H u = x) \to u H y = y)$
13		simpr	$⊢ (y H x = x \land x H y = x) \to x H y = x$
14	13	ralimi	$⊢ \forall x \in X (y H x = x \land x H y = x) \to \forall x \in X x H y = x$
15		oveq1	$⊢ x = u \to x H y = u H y$
16		id	$⊢ x = u \to x = u$
17	15 16	eqeq12d	$⊢ x = u \to (x H y = x \leftrightarrow u H y = u)$
18	17	rspcv	$⊢ u \in X \to (\forall x \in X x H y = x \to u H y = u)$
19	14 18	syl5	$⊢ u \in X \to (\forall x \in X (y H x = x \land x H y = x) \to u H y = u)$
20	12 19	im2anan9r	$⊢ (u \in X \land y \in X) \to ((\forall x \in X (u H x = x \land x H u = x) \land \forall x \in X (y H x = x \land x H y = x)) \to (u H y = y \land u H y = u))$
21		eqtr2	$⊢ (u H y = y \land u H y = u) \to y = u$
22	21	equcomd	$⊢ (u H y = y \land u H y = u) \to u = y$
23	20 22	syl6	$⊢ (u \in X \land y \in X) \to ((\forall x \in X (u H x = x \land x H u = x) \land \forall x \in X (y H x = x \land x H y = x)) \to u = y)$
24	23	rgen2	$⊢ \forall u \in X \forall y \in X ((\forall x \in X (u H x = x \land x H u = x) \land \forall x \in X (y H x = x \land x H y = x)) \to u = y)$
25		oveq1	$⊢ u = y \to u H x = y H x$
26	25	eqeq1d	$⊢ u = y \to (u H x = x \leftrightarrow y H x = x)$
27	26	ovanraleqv	$⊢ u = y \to (\forall x \in X (u H x = x \land x H u = x) \leftrightarrow \forall x \in X (y H x = x \land x H y = x))$
28	27	reu4	$⊢ \exists! u \in X \forall x \in X (u H x = x \land x H u = x) \leftrightarrow (\exists u \in X \forall x \in X (u H x = x \land x H u = x) \land \forall u \in X \forall y \in X ((\forall x \in X (u H x = x \land x H u = x) \land \forall x \in X (y H x = x \land x H y = x)) \to u = y))$
29	5 24 28	sylanblrc	$⊢ R \in RingOps \to \exists! u \in X \forall x \in X (u H x = x \land x H u = x)$

Metamath Proof Explorer

Theorem rngoideu

Proof