dvrcan1

Description: A cancellation law for division. ( divcan1 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014)

	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	dvrcan1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} 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		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
6	1 4 2 5 3	dvrval	$⊢ (X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
7	6	3adant1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
8	7	oveq1d	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} Y = (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} Y$
9		simp1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to R \in Ring$
10		simp2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \in B$
11	2 5 1	ringinvcl	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \in B$
12	11	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to {inv}_{r} (R) (Y) \in B$
13	1 2	unitcl	$⊢ Y \in U \to Y \in B$
14	13	3ad2ant3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to Y \in B$
15	1 4	ringass	$⊢ (R \in Ring \land (X \in B \land {inv}_{r} (R) (Y) \in B \land Y \in B)) \to (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} Y)$
16	9 10 12 14 15	syl13anc	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} Y)$
17		eqid	$⊢ 1_{R} = 1_{R}$
18	2 5 4 17	unitlinv	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \underset{˙}{\cdot} Y = 1_{R}$
19	18	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to {inv}_{r} (R) (Y) \underset{˙}{\cdot} Y = 1_{R}$
20	19	oveq2d	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} 1_{R}$
21	1 4 17	ringridm	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} 1_{R} = X$
22	21	3adant3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\cdot} 1_{R} = X$
23	20 22	eqtrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} Y) = X$
24	16 23	eqtrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} Y = X$
25	8 24	eqtrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} Y = X$

Metamath Proof Explorer

Theorem dvrcan1

Proof