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

Metamath Proof Explorer

Theorem unitmulcl

Description: The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitmulcl.2 ⊢ · = ( .r ‘ 𝑅 )
Assertion unitmulcl ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitmulcl.2 ⊢ · = ( .r ‘ 𝑅 )
3 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring )
4 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 1 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ ( Base ‘ 𝑅 ) )
7 4 6 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Base ‘ 𝑅 ) )
8 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
11 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
12 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
13 1 9 10 11 12 isunit ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
14 8 13 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
15 14 simpld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
16 5 10 2 dvdsrmul1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
17 3 7 15 16 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
18 5 2 9 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
19 3 7 18 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
20 17 19 breqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) 𝑌 )
21 1 9 10 11 12 isunit ⊢ ( 𝑌 ∈ 𝑈 ↔ ( 𝑌 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑌 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
22 4 21 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑌 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
23 22 simpld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
24 5 10 dvdsrtr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) 𝑌 ∧ 𝑌 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
25 3 20 23 24 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
26 11 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
27 3 26 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( oppr ‘ 𝑅 ) ∈ Ring )
28 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
29 5 2 11 28 opprmul ⊢ ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · 𝑌 )
30 5 1 unitcl ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
31 8 30 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
32 22 simprd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
33 11 5 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
34 33 12 28 dvdsrmul1 ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( 1r ‘ 𝑅 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) )
35 27 31 32 34 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( 1r ‘ 𝑅 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) )
36 5 2 11 28 opprmul ⊢ ( ( 1r ‘ 𝑅 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · ( 1r ‘ 𝑅 ) )
37 5 2 9 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
38 3 31 37 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
39 36 38 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 𝑋 )
40 35 39 breqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 )
41 29 40 eqbrtrrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 )
42 14 simprd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
43 33 12 dvdsrtr ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑋 · 𝑌 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
44 27 41 42 43 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
45 1 9 10 11 12 isunit ⊢ ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ↔ ( ( 𝑋 · 𝑌 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ ( 𝑋 · 𝑌 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
46 25 44 45 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )