This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngolidm

Description: The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-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	rngolidm	$⊢ (R \in RingOps \land A \in X) \to U H A = 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 2 3	rngoidmlem	$⊢ (R \in RingOps \land A \in X) \to (U H A = A \land A H U = A)$
5	4	simpld	$⊢ (R \in RingOps \land A \in X) \to U H A = A$