unitmulclb

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

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

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	$⊢ U = Unit (R)$
2		unitmulcl.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		unitmulclb.1	$⊢ B = {Base}_{R}$
4		simp1	$⊢ (R \in CRing \land X \in B \land Y \in B) \to R \in CRing$
5		simp2	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ (R \in CRing \land X \in B \land Y \in B) \to Y \in B$
7		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
8	3 7 2	dvdsrmul	$⊢ (X \in B \land Y \in B) \to X ∥_{r} (R) (Y \underset{˙}{\cdot} X)$
9	5 6 8	syl2anc	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X ∥_{r} (R) (Y \underset{˙}{\cdot} X)$
10	3 2	crngcom	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
11	9 10	breqtrrd	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X ∥_{r} (R) (X \underset{˙}{\cdot} Y)$
12	1 7	dvdsunit	$⊢ (R \in CRing \land X ∥_{r} (R) (X \underset{˙}{\cdot} Y) \land X \underset{˙}{\cdot} Y \in U) \to X \in U$
13	12	3expia	$⊢ (R \in CRing \land X ∥_{r} (R) (X \underset{˙}{\cdot} Y)) \to (X \underset{˙}{\cdot} Y \in U \to X \in U)$
14	4 11 13	syl2anc	$⊢ (R \in CRing \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y \in U \to X \in U)$
15	3 7 2	dvdsrmul	$⊢ (Y \in B \land X \in B) \to Y ∥_{r} (R) (X \underset{˙}{\cdot} Y)$
16	6 5 15	syl2anc	$⊢ (R \in CRing \land X \in B \land Y \in B) \to Y ∥_{r} (R) (X \underset{˙}{\cdot} Y)$
17	1 7	dvdsunit	$⊢ (R \in CRing \land Y ∥_{r} (R) (X \underset{˙}{\cdot} Y) \land X \underset{˙}{\cdot} Y \in U) \to Y \in U$
18	17	3expia	$⊢ (R \in CRing \land Y ∥_{r} (R) (X \underset{˙}{\cdot} Y)) \to (X \underset{˙}{\cdot} Y \in U \to Y \in U)$
19	4 16 18	syl2anc	$⊢ (R \in CRing \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y \in U \to Y \in U)$
20	14 19	jcad	$⊢ (R \in CRing \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y \in U \to (X \in U \land Y \in U))$
21		crngring	$⊢ R \in CRing \to R \in Ring$
22	21	3ad2ant1	$⊢ (R \in CRing \land X \in B \land Y \in B) \to R \in Ring$
23	1 2	unitmulcl	$⊢ (R \in Ring \land X \in U \land Y \in U) \to X \underset{˙}{\cdot} Y \in U$
24	23	3expib	$⊢ R \in Ring \to ((X \in U \land Y \in U) \to X \underset{˙}{\cdot} Y \in U)$
25	22 24	syl	$⊢ (R \in CRing \land X \in B \land Y \in B) \to ((X \in U \land Y \in U) \to X \underset{˙}{\cdot} Y \in U)$
26	20 25	impbid	$⊢ (R \in CRing \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y \in U \leftrightarrow (X \in U \land Y \in U))$

Metamath Proof Explorer

Theorem unitmulclb

Proof