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	syl5eq	⊢ ( ( 𝑅 ∈ 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 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )