dvrcl

Description: Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Step	Hyp	Ref	Expression
1		dvrcl.b	$⊢ B = {Base}_{R}$
2		dvrcl.o	$⊢ U = Unit (R)$
3		dvrcl.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
4		eqid	$⊢ \cdot_{R} = \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 \cdot_{R} {inv}_{r} (R) (Y)$
7	6	3adant1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
8	2 5 1	ringinvcl	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \in B$
9	8	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to {inv}_{r} (R) (Y) \in B$
10	1 4	ringcl	$⊢ (R \in Ring \land X \in B \land {inv}_{r} (R) (Y) \in B) \to X \cdot_{R} {inv}_{r} (R) (Y) \in B$
11	9 10	syld3an3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \cdot_{R} {inv}_{r} (R) (Y) \in B$
12	7 11	eqeltrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \underset{˙}{\times} Y \in B$

Metamath Proof Explorer