This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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