Metamath Proof Explorer

Theorem dvrcan3

Description: A cancellation law for division. ( divcan3 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 18-Jun-2015)

		Ref	Expression
	Hypotheses	dvrass.b	$⊢ B = {Base}_{R}$
		dvrass.o	$⊢ U = Unit (R)$
		dvrass.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
		dvrass.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	dvrcan3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Y = X$

Proof

Step	Hyp	Ref	Expression
1		dvrass.b	$⊢ B = {Base}_{R}$
2		dvrass.o	$⊢ U = Unit (R)$
3		dvrass.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
4		dvrass.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simp1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to R \in Ring$
6		simp2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \in B$
7	1 2	unitcl	$⊢ Y \in U \to Y \in B$
8	7	3ad2ant3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to Y \in B$
9		simp3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to Y \in U$
10	1 2 3 4	dvrass	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Y \in U)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Y = X \underset{˙}{\cdot} (Y \underset{˙}{\times} Y)$
11	5 6 8 9 10	syl13anc	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Y = X \underset{˙}{\cdot} (Y \underset{˙}{\times} Y)$
12		eqid	$⊢ 1_{R} = 1_{R}$
13	2 3 12	dvrid	$⊢ (R \in Ring \land Y \in U) \to Y \underset{˙}{\times} Y = 1_{R}$
14	13	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to Y \underset{˙}{\times} Y = 1_{R}$
15	14	oveq2d	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\cdot} (Y \underset{˙}{\times} Y) = X \underset{˙}{\cdot} 1_{R}$
16	1 4 12	ringridm	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} 1_{R} = X$
17	16	3adant3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\cdot} 1_{R} = X$
18	11 15 17	3eqtrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Y = X$