isringid

Description: Properties showing that an element I is the unity element of a ring. (Contributed by NM, 7-Aug-2013)

	Ref	Expression
Hypotheses	ringidm.b	$⊢ B = {Base}_{R}$
	ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	isringid	$⊢ R \in Ring \to ((I \in B \land \forall x \in B (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \leftrightarrow \underset{˙}{1} = I)$

Step	Hyp	Ref	Expression
1		ringidm.b	$⊢ B = {Base}_{R}$
2		ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
6	4 3	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
7	4 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
8	1 2	ringideu	$⊢ R \in Ring \to \exists! y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
9		reurex	$⊢ \exists! y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x) \to \exists y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
10	8 9	syl	$⊢ R \in Ring \to \exists y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
11	5 6 7 10	ismgmid	$⊢ R \in Ring \to ((I \in B \land \forall x \in B (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \leftrightarrow \underset{˙}{1} = I)$

Metamath Proof Explorer