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

Metamath Proof Explorer

Theorem dfur2

Description: The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015)

		Ref	Expression
	Hypotheses	dfur2.b	$⊢ B = {Base}_{R}$
		dfur2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		dfur2.u	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	dfur2	$⊢ \underset{˙}{1} = (ι e \| (e \in B \land \forall x \in B (e \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} e = x)))$

Proof

Step	Hyp	Ref	Expression
1		dfur2.b	$⊢ B = {Base}_{R}$
2		dfur2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		dfur2.u	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
6	4 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
7	4 3	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
8	5 6 7	grpidval	$⊢ \underset{˙}{1} = (ι e \| (e \in B \land \forall x \in B (e \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} e = x)))$