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

Metamath Proof Explorer

Theorem unitmulclb

Description: Reversal of unitmulcl in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitmulcl.2 ⊢ · = ( .r ‘ 𝑅 )
unitmulclb.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion unitmulclb ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitmulcl.2 ⊢ · = ( .r ‘ 𝑅 )
3 unitmulclb.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 simp1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ CRing )
5 simp2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
6 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
7 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
8 3 7 2 dvdsrmul ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑌 · 𝑋 ) )
9 5 6 8 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑌 · 𝑋 ) )
10 3 2 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )
11 9 10 breqtrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
12 1 7 dvdsunit ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ ( 𝑋 · 𝑌 ) ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
13 12 3expia ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → 𝑋 ∈ 𝑈 ) )
14 4 11 13 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → 𝑋 ∈ 𝑈 ) )
15 3 7 2 dvdsrmul ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝑌 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
16 6 5 15 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
17 1 7 dvdsunit ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ ( 𝑋 · 𝑌 ) ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
18 17 3expia ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ( ∥r ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )
19 4 16 18 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )
20 14 19 jcad ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) )
21 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 21 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
23 1 2 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )
24 23 3expib ⊢ ( 𝑅 ∈ Ring → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 ) )
25 22 24 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 ) )
26 20 25 impbid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) )