dvrid

Description: A ring element divided by itself is the ring unity. ( divid analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	unitdvcl.o	$⊢ U = Unit (R)$
	unitdvcl.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
	dvrid.o	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	dvrid	$⊢ (R \in Ring \land X \in U) \to X \underset{˙}{\times} X = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		unitdvcl.o	$⊢ U = Unit (R)$
2		unitdvcl.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		dvrid.o	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4 1	unitcl	$⊢ X \in U \to X \in {Base}_{R}$
6	5	adantl	$⊢ (R \in Ring \land X \in U) \to X \in {Base}_{R}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
9	4 7 1 8 2	dvrval	$⊢ (X \in {Base}_{R} \land X \in U) \to X \underset{˙}{\times} X = X \cdot_{R} {inv}_{r} (R) (X)$
10	6 9	sylancom	$⊢ (R \in Ring \land X \in U) \to X \underset{˙}{\times} X = X \cdot_{R} {inv}_{r} (R) (X)$
11	1 8 7 3	unitrinv	$⊢ (R \in Ring \land X \in U) \to X \cdot_{R} {inv}_{r} (R) (X) = \underset{˙}{1}$
12	10 11	eqtrd	$⊢ (R \in Ring \land X \in U) \to X \underset{˙}{\times} X = \underset{˙}{1}$

Metamath Proof Explorer