Metamath Proof Explorer

Theorem rngoid

Description: The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-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	rngoid	$⊢ (R \in RingOps \land A \in X) \to \exists u \in X (u H A = A \land A H u = A)$

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		r19.12	$⊢ \exists u \in X \forall x \in X (u H x = x \land x H u = x) \to \forall x \in X \exists u \in X (u H x = x \land x H u = x)$
7	5 6	syl	$⊢ R \in RingOps \to \forall x \in X \exists u \in X (u H x = x \land x H u = x)$
8		oveq2	$⊢ x = A \to u H x = u H A$
9		id	$⊢ x = A \to x = A$
10	8 9	eqeq12d	$⊢ x = A \to (u H x = x \leftrightarrow u H A = A)$
11		oveq1	$⊢ x = A \to x H u = A H u$
12	11 9	eqeq12d	$⊢ x = A \to (x H u = x \leftrightarrow A H u = A)$
13	10 12	anbi12d	$⊢ x = A \to ((u H x = x \land x H u = x) \leftrightarrow (u H A = A \land A H u = A))$
14	13	rexbidv	$⊢ x = A \to (\exists u \in X (u H x = x \land x H u = x) \leftrightarrow \exists u \in X (u H A = A \land A H u = A))$
15	14	rspccva	$⊢ (\forall x \in X \exists u \in X (u H x = x \land x H u = x) \land A \in X) \to \exists u \in X (u H A = A \land A H u = A)$
16	7 15	sylan	$⊢ (R \in RingOps \land A \in X) \to \exists u \in X (u H A = A \land A H u = A)$