Metamath Proof Explorer


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 ∧ 𝑌 𝑋𝑋𝑈 ) → 𝑌𝑈 )