Theorem dvdsunit

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

	Ref	Expression
Hypotheses	dvdsunit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	dvdsunit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	dvdsunit	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\wedge X\in U\right)\to Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		dvdsunit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		dvdsunit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4 2	dvdsrtr	$$⊢\left(R\in \mathrm{Ring}\wedge Y\underset{\dot{}}{\parallel }X\wedge X\underset{\dot{}}{\parallel }{1}_R\right)\to Y\underset{\dot{}}{\parallel }{1}_R$$
6	5	3expia	$$⊢\left(R\in \mathrm{Ring}\wedge Y\underset{\dot{}}{\parallel }X\right)\to \left(X\underset{\dot{}}{\parallel }{1}_R\to Y\underset{\dot{}}{\parallel }{1}_R\right)$$
7	3 6	sylan	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\right)\to \left(X\underset{\dot{}}{\parallel }{1}_R\to Y\underset{\dot{}}{\parallel }{1}_R\right)$$
8		eqid	$$⊢1_R=1_R$$
9	1 8 2	crngunit	$$⊢R\in \mathrm{CRing}\to \left(X\in U\leftrightarrow X\underset{\dot{}}{\parallel }{1}_R\right)$$
10	9	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\right)\to \left(X\in U\leftrightarrow X\underset{\dot{}}{\parallel }{1}_R\right)$$
11	1 8 2	crngunit	$$⊢R\in \mathrm{CRing}\to \left(Y\in U\leftrightarrow Y\underset{\dot{}}{\parallel }{1}_R\right)$$
12	11	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\right)\to \left(Y\in U\leftrightarrow Y\underset{\dot{}}{\parallel }{1}_R\right)$$
13	7 10 12	3imtr4d	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\right)\to \left(X\in U\to Y\in U\right)$$
14	13	3impia	$$⊢\left(R\in \mathrm{CRing}\wedge Y\underset{\dot{}}{\parallel }X\wedge X\in U\right)\to Y\in U$$