unitmulcl

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

	Ref	Expression
Hypotheses	unitmulcl.1	$⊢ U = Unit (R)$
	unitmulcl.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	unitmulcl	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\cdot} Y \in U$

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	$⊢ U = Unit (R)$
2		unitmulcl.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		simp1	$⊢ (R \in Ring \land X \in U \land Y \in U) \to R \in Ring$
4		simp3	$⊢ (R \in Ring \land X \in U \land Y \in U) \to Y \in U$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 1	unitcl	$⊢ Y \in U \to Y \in {Base}_{R}$
7	4 6	syl	$⊢ (R \in Ring \land X \in U \land Y \in U) \to Y \in {Base}_{R}$
8		simp2	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \in U$
9		eqid	$⊢ 1_{R} = 1_{R}$
10		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
11		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
12		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
13	1 9 10 11 12	isunit	$⊢ X \in U \leftrightarrow (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
14	8 13	sylib	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
15	14	simpld	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X ∥_{r} (R) 1_{R}$
16	5 10 2	dvdsrmul1	$⊢ (R \in Ring \land Y \in {Base}_{R} \land X ∥_{r} (R) 1_{R}) \to (X \underset{˙}{\cdot} Y) ∥_{r} (R) (1_{R} \underset{˙}{\cdot} Y)$
17	3 7 15 16	syl3anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) ∥_{r} (R) (1_{R} \underset{˙}{\cdot} Y)$
18	5 2 9	ringlidm	$⊢ (R \in Ring \land Y \in {Base}_{R}) \to 1_{R} \underset{˙}{\cdot} Y = Y$
19	3 7 18	syl2anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to 1_{R} \underset{˙}{\cdot} Y = Y$
20	17 19	breqtrd	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) ∥_{r} (R) Y$
21	1 9 10 11 12	isunit	$⊢ Y \in U \leftrightarrow (Y ∥_{r} (R) 1_{R} \land Y ∥_{r} ({opp}_{r} (R)) 1_{R})$
22	4 21	sylib	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (Y ∥_{r} (R) 1_{R} \land Y ∥_{r} ({opp}_{r} (R)) 1_{R})$
23	22	simpld	$⊢ (R \in Ring \land X \in U \land Y \in U) \to Y ∥_{r} (R) 1_{R}$
24	5 10	dvdsrtr	$⊢ (R \in Ring \land (X \underset{˙}{\cdot} Y) ∥_{r} (R) Y \land Y ∥_{r} (R) 1_{R}) \to (X \underset{˙}{\cdot} Y) ∥_{r} (R) 1_{R}$
25	3 20 23 24	syl3anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) ∥_{r} (R) 1_{R}$
26	11	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
27	3 26	syl	$⊢ (R \in Ring \land X \in U \land Y \in U) \to {opp}_{r} (R) \in Ring$
28		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
29	5 2 11 28	opprmul	$⊢ Y \cdot_{{opp}_{r} (R)} X = X \underset{˙}{\cdot} Y$
30	5 1	unitcl	$⊢ X \in U \to X \in {Base}_{R}$
31	8 30	syl	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \in {Base}_{R}$
32	22	simprd	$⊢ (R \in Ring \land X \in U \land Y \in U) \to Y ∥_{r} ({opp}_{r} (R)) 1_{R}$
33	11 5	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
34	33 12 28	dvdsrmul1	$⊢ ({opp}_{r} (R) \in Ring \land X \in {Base}_{R} \land Y ∥_{r} ({opp}_{r} (R)) 1_{R}) \to (Y \cdot_{{opp}_{r} (R)} X) ∥_{r} ({opp}_{r} (R)) (1_{R} \cdot_{{opp}_{r} (R)} X)$
35	27 31 32 34	syl3anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (Y \cdot_{{opp}_{r} (R)} X) ∥_{r} ({opp}_{r} (R)) (1_{R} \cdot_{{opp}_{r} (R)} X)$
36	5 2 11 28	opprmul	$⊢ 1_{R} \cdot_{{opp}_{r} (R)} X = X \underset{˙}{\cdot} 1_{R}$
37	5 2 9	ringridm	$⊢ (R \in Ring \land X \in {Base}_{R}) \to X \underset{˙}{\cdot} 1_{R} = X$
38	3 31 37	syl2anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\cdot} 1_{R} = X$
39	36 38	syl5eq	$⊢ (R \in Ring \land X \in U \land Y \in U) \to 1_{R} \cdot_{{opp}_{r} (R)} X = X$
40	35 39	breqtrd	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (Y \cdot_{{opp}_{r} (R)} X) ∥_{r} ({opp}_{r} (R)) X$
41	29 40	eqbrtrrid	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) ∥_{r} ({opp}_{r} (R)) X$
42	14	simprd	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X ∥_{r} ({opp}_{r} (R)) 1_{R}$
43	33 12	dvdsrtr	$⊢ ({opp}_{r} (R) \in Ring \land (X \underset{˙}{\cdot} Y) ∥_{r} ({opp}_{r} (R)) X \land X ∥_{r} ({opp}_{r} (R)) 1_{R}) \to (X \underset{˙}{\cdot} Y) ∥_{r} ({opp}_{r} (R)) 1_{R}$
44	27 41 42 43	syl3anc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) ∥_{r} ({opp}_{r} (R)) 1_{R}$
45	1 9 10 11 12	isunit	$⊢ X \underset{˙}{\cdot} Y \in U \leftrightarrow ((X \underset{˙}{\cdot} Y) ∥_{r} (R) 1_{R} \land (X \underset{˙}{\cdot} Y) ∥_{r} ({opp}_{r} (R)) 1_{R})$
46	25 44 45	sylanbrc	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\cdot} Y \in U$

Metamath Proof Explorer

Theorem unitmulcl

Proof