Metamath Proof Explorer

Theorem ringid

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) (Revised by AV, 24-Aug-2021)

		Ref	Expression
	Hypotheses	ringid.b	$⊢ B = {Base}_{R}$
		ringid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	ringid	$⊢ (R \in Ring \land X \in B) \to \exists u \in B (u \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} u = X)$

Proof

Step	Hyp	Ref	Expression
1		ringid.b	$⊢ B = {Base}_{R}$
2		ringid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	1 3	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
5	4	adantr	$⊢ (R \in Ring \land X \in B) \to 1_{R} \in B$
6		oveq1	$⊢ u = 1_{R} \to u \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
7	6	eqeq1d	$⊢ u = 1_{R} \to (u \underset{˙}{\cdot} X = X \leftrightarrow 1_{R} \underset{˙}{\cdot} X = X)$
8		oveq2	$⊢ u = 1_{R} \to X \underset{˙}{\cdot} u = X \underset{˙}{\cdot} 1_{R}$
9	8	eqeq1d	$⊢ u = 1_{R} \to (X \underset{˙}{\cdot} u = X \leftrightarrow X \underset{˙}{\cdot} 1_{R} = X)$
10	7 9	anbi12d	$⊢ u = 1_{R} \to ((u \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} u = X) \leftrightarrow (1_{R} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} 1_{R} = X))$
11	10	adantl	$⊢ ((R \in Ring \land X \in B) \land u = 1_{R}) \to ((u \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} u = X) \leftrightarrow (1_{R} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} 1_{R} = X))$
12	1 2 3	ringidmlem	$⊢ (R \in Ring \land X \in B) \to (1_{R} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} 1_{R} = X)$
13	5 11 12	rspcedvd	$⊢ (R \in Ring \land X \in B) \to \exists u \in B (u \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} u = X)$