Theorem dvdsunit

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

	Ref	Expression
Hypotheses	dvdsunit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	dvdsunit.3	⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion	dvdsunit	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		dvdsunit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		dvdsunit.3	⊢ ∥ = ( ∥r ‘ 𝑅 )
3		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	4 2	dvdsrtr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∥ ( 1r ‘ 𝑅 ) ) → 𝑌 ∥ ( 1r ‘ 𝑅 ) )
6	5	3expia	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑋 ) → ( 𝑋 ∥ ( 1r ‘ 𝑅 ) → 𝑌 ∥ ( 1r ‘ 𝑅 ) ) )
7	3 6	sylan	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ) → ( 𝑋 ∥ ( 1r ‘ 𝑅 ) → 𝑌 ∥ ( 1r ‘ 𝑅 ) ) )
8		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9	1 8 2	crngunit	⊢ ( 𝑅 ∈ CRing → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∥ ( 1r ‘ 𝑅 ) ) )
10	9	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ) → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∥ ( 1r ‘ 𝑅 ) ) )
11	1 8 2	crngunit	⊢ ( 𝑅 ∈ CRing → ( 𝑌 ∈ 𝑈 ↔ 𝑌 ∥ ( 1r ‘ 𝑅 ) ) )
12	11	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ) → ( 𝑌 ∈ 𝑈 ↔ 𝑌 ∥ ( 1r ‘ 𝑅 ) ) )
13	7 10 12	3imtr4d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ) → ( 𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )
14	13	3impia	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ 𝑋 ∧ 𝑋 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )