rngoidmlem

Description: The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		uridm.1	$⊢ H = 2^{nd} (R)$
2		uridm.2	$⊢ X = ran 1^{st} (R)$
3		uridm.3	$⊢ U = GId (H)$
4	1	rngomndo	$⊢ R \in RingOps \to H \in MndOp$
5		mndomgmid	$⊢ H \in MndOp \to H \in (Magma \cap ExId)$
6		eqid	$⊢ ran H = ran H$
7	6 3	cmpidelt	$⊢ (H \in (Magma \cap ExId) \land A \in ran H) \to (U H A = A \land A H U = A)$
8	7	ex	$⊢ H \in (Magma \cap ExId) \to (A \in ran H \to (U H A = A \land A H U = A))$
9	4 5 8	3syl	$⊢ R \in RingOps \to (A \in ran H \to (U H A = A \land A H U = A))$
10		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
11	1 10	rngorn1eq	$⊢ R \in RingOps \to ran 1^{st} (R) = ran H$
12		eqtr	$⊢ (X = ran 1^{st} (R) \land ran 1^{st} (R) = ran H) \to X = ran H$
13		simpl	$⊢ (X = ran H \land R \in RingOps) \to X = ran H$
14	13	eleq2d	$⊢ (X = ran H \land R \in RingOps) \to (A \in X \leftrightarrow A \in ran H)$
15	14	imbi1d	$⊢ (X = ran H \land R \in RingOps) \to ((A \in X \to (U H A = A \land A H U = A)) \leftrightarrow (A \in ran H \to (U H A = A \land A H U = A)))$
16	15	ex	$⊢ X = ran H \to (R \in RingOps \to ((A \in X \to (U H A = A \land A H U = A)) \leftrightarrow (A \in ran H \to (U H A = A \land A H U = A))))$
17	12 16	syl	$⊢ (X = ran 1^{st} (R) \land ran 1^{st} (R) = ran H) \to (R \in RingOps \to ((A \in X \to (U H A = A \land A H U = A)) \leftrightarrow (A \in ran H \to (U H A = A \land A H U = A))))$
18	2 17	mpan	$⊢ ran 1^{st} (R) = ran H \to (R \in RingOps \to ((A \in X \to (U H A = A \land A H U = A)) \leftrightarrow (A \in ran H \to (U H A = A \land A H U = A))))$
19	11 18	mpcom	$⊢ R \in RingOps \to ((A \in X \to (U H A = A \land A H U = A)) \leftrightarrow (A \in ran H \to (U H A = A \land A H U = A)))$
20	9 19	mpbird	$⊢ R \in RingOps \to (A \in X \to (U H A = A \land A H U = A))$
21	20	imp	$⊢ (R \in RingOps \land A \in X) \to (U H A = A \land A H U = A)$

Metamath Proof Explorer

Theorem rngoidmlem

Proof