dvdsunit

Description: A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dvdsunit.1	$⊢ U = Unit (R)$
	dvdsunit.3	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	dvdsunit	$⊢ (R \in CRing \land Y \underset{˙}{∥} X \land X \in U) \to Y \in U$

Step	Hyp	Ref	Expression
1		dvdsunit.1	$⊢ U = Unit (R)$
2		dvdsunit.3	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4 2	dvdsrtr	$⊢ (R \in Ring \land Y \underset{˙}{∥} X \land X \underset{˙}{∥} 1_{R}) \to Y \underset{˙}{∥} 1_{R}$
6	5	3expia	$⊢ (R \in Ring \land Y \underset{˙}{∥} X) \to (X \underset{˙}{∥} 1_{R} \to Y \underset{˙}{∥} 1_{R})$
7	3 6	sylan	$⊢ (R \in CRing \land Y \underset{˙}{∥} X) \to (X \underset{˙}{∥} 1_{R} \to Y \underset{˙}{∥} 1_{R})$
8		eqid	$⊢ 1_{R} = 1_{R}$
9	1 8 2	crngunit	$⊢ R \in CRing \to (X \in U \leftrightarrow X \underset{˙}{∥} 1_{R})$
10	9	adantr	$⊢ (R \in CRing \land Y \underset{˙}{∥} X) \to (X \in U \leftrightarrow X \underset{˙}{∥} 1_{R})$
11	1 8 2	crngunit	$⊢ R \in CRing \to (Y \in U \leftrightarrow Y \underset{˙}{∥} 1_{R})$
12	11	adantr	$⊢ (R \in CRing \land Y \underset{˙}{∥} X) \to (Y \in U \leftrightarrow Y \underset{˙}{∥} 1_{R})$
13	7 10 12	3imtr4d	$⊢ (R \in CRing \land Y \underset{˙}{∥} X) \to (X \in U \to Y \in U)$
14	13	3impia	$⊢ (R \in CRing \land Y \underset{˙}{∥} X \land X \in U) \to Y \in U$

Metamath Proof Explorer