dvr1

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

	Ref	Expression
Hypotheses	dvr1.b	$⊢ B = {Base}_{R}$
	dvr1.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
	dvr1.o	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	dvr1	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\times} \underset{˙}{1} = X$

Step	Hyp	Ref	Expression
1		dvr1.b	$⊢ B = {Base}_{R}$
2		dvr1.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		dvr1.o	$⊢ \underset{˙}{1} = 1_{R}$
4		id	$⊢ X \in B \to X \in B$
5		eqid	$⊢ Unit (R) = Unit (R)$
6	5 3	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in Unit (R)$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
9	1 7 5 8 2	dvrval	$⊢ (X \in B \land \underset{˙}{1} \in Unit (R)) \to X \underset{˙}{\times} \underset{˙}{1} = X \cdot_{R} {inv}_{r} (R) (\underset{˙}{1})$
10	4 6 9	syl2anr	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\times} \underset{˙}{1} = X \cdot_{R} {inv}_{r} (R) (\underset{˙}{1})$
11	8 3	1rinv	$⊢ R \in Ring \to {inv}_{r} (R) (\underset{˙}{1}) = \underset{˙}{1}$
12	11	adantr	$⊢ (R \in Ring \land X \in B) \to {inv}_{r} (R) (\underset{˙}{1}) = \underset{˙}{1}$
13	12	oveq2d	$⊢ (R \in Ring \land X \in B) \to X \cdot_{R} {inv}_{r} (R) (\underset{˙}{1}) = X \cdot_{R} \underset{˙}{1}$
14	1 7 3	ringridm	$⊢ (R \in Ring \land X \in B) \to X \cdot_{R} \underset{˙}{1} = X$
15	10 13 14	3eqtrd	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\times} \underset{˙}{1} = X$

Metamath Proof Explorer