unitdvcl

Description: The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Step	Hyp	Ref	Expression
1		unitdvcl.o	$⊢ U = Unit (R)$
2		unitdvcl.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 1	unitcl	$⊢ X \in U \to X \in {Base}_{R}$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
7	3 5 1 6 2	dvrval	$⊢ (X \in {Base}_{R} \land Y \in U) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
8	4 7	sylan	$⊢ (X \in U \land Y \in U) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
9	8	3adant1	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
10	1 6	unitinvcl	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \in U$
11	10	3adant2	$⊢ (R \in Ring \land X \in U \land Y \in U) \to {inv}_{r} (R) (Y) \in U$
12	1 5	unitmulcl	$⊢ (R \in Ring \land X \in U \land {inv}_{r} (R) (Y) \in U) \to X \cdot_{R} {inv}_{r} (R) (Y) \in U$
13	11 12	syld3an3	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \cdot_{R} {inv}_{r} (R) (Y) \in U$
14	9 13	eqeltrd	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\times} Y \in U$

Metamath Proof Explorer