unitpidl1

Description: The ideal I generated by an element X of an integral domain R is the unit ideal B iff X is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	unitpidl1.1	$⊢ U = Unit (R)$
	unitpidl1.2	$⊢ K = RSpan (R)$
	unitpidl1.3	$⊢ I = K (\{X\})$
	unitpidl1.4	$⊢ B = {Base}_{R}$
	unitpidl1.5	$⊢ φ \to X \in B$
	unitpidl1.6	$⊢ φ \to R \in IDomn$
Assertion	unitpidl1	$⊢ φ \to (I = B \leftrightarrow X \in U)$

Proof

Step	Hyp	Ref	Expression
1		unitpidl1.1	$⊢ U = Unit (R)$
2		unitpidl1.2	$⊢ K = RSpan (R)$
3		unitpidl1.3	$⊢ I = K (\{X\})$
4		unitpidl1.4	$⊢ B = {Base}_{R}$
5		unitpidl1.5	$⊢ φ \to X \in B$
6		unitpidl1.6	$⊢ φ \to R \in IDomn$
7		df-idom	$⊢ IDomn = CRing \cap Domn$
8	6 7	eleqtrdi	$⊢ φ \to R \in (CRing \cap Domn)$
9	8	elin1d	$⊢ φ \to R \in CRing$
10	9	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to R \in CRing$
11		simplr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to y \in B$
12	5	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to X \in B$
13		simpr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to 1_{R} = y \cdot_{R} X$
14	6	idomringd	$⊢ φ \to R \in Ring$
15		eqid	$⊢ 1_{R} = 1_{R}$
16	1 15	1unit	$⊢ R \in Ring \to 1_{R} \in U$
17	14 16	syl	$⊢ φ \to 1_{R} \in U$
18	17	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to 1_{R} \in U$
19	13 18	eqeltrrd	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to y \cdot_{R} X \in U$
20		eqid	$⊢ \cdot_{R} = \cdot_{R}$
21	1 20 4	unitmulclb	$⊢ (R \in CRing \land y \in B \land X \in B) \to (y \cdot_{R} X \in U \leftrightarrow (y \in U \land X \in U))$
22	21	simplbda	$⊢ ((R \in CRing \land y \in B \land X \in B) \land y \cdot_{R} X \in U) \to X \in U$
23	10 11 12 19 22	syl31anc	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to X \in U$
24	14	adantr	$⊢ (φ \land I = B) \to R \in Ring$
25	5	adantr	$⊢ (φ \land I = B) \to X \in B$
26	5	snssd	$⊢ φ \to \{X\} \subseteq B$
27		eqid	$⊢ LIdeal (R) = LIdeal (R)$
28	2 4 27	rspcl	$⊢ (R \in Ring \land \{X\} \subseteq B) \to K (\{X\}) \in LIdeal (R)$
29	14 26 28	syl2anc	$⊢ φ \to K (\{X\}) \in LIdeal (R)$
30	3 29	eqeltrid	$⊢ φ \to I \in LIdeal (R)$
31	30	adantr	$⊢ (φ \land I = B) \to I \in LIdeal (R)$
32		simpr	$⊢ (φ \land I = B) \to I = B$
33	27 4 15	lidl1el	$⊢ (R \in Ring \land I \in LIdeal (R)) \to (1_{R} \in I \leftrightarrow I = B)$
34	33	biimpar	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land I = B) \to 1_{R} \in I$
35	24 31 32 34	syl21anc	$⊢ (φ \land I = B) \to 1_{R} \in I$
36	35 3	eleqtrdi	$⊢ (φ \land I = B) \to 1_{R} \in K (\{X\})$
37	4 20 2	elrspsn	$⊢ (R \in Ring \land X \in B) \to (1_{R} \in K (\{X\}) \leftrightarrow \exists y \in B 1_{R} = y \cdot_{R} X)$
38	37	biimpa	$⊢ ((R \in Ring \land X \in B) \land 1_{R} \in K (\{X\})) \to \exists y \in B 1_{R} = y \cdot_{R} X$
39	24 25 36 38	syl21anc	$⊢ (φ \land I = B) \to \exists y \in B 1_{R} = y \cdot_{R} X$
40	23 39	r19.29a	$⊢ (φ \land I = B) \to X \in U$
41		simpr	$⊢ (φ \land X \in U) \to X \in U$
42	2 4	rspssid	$⊢ (R \in Ring \land \{X\} \subseteq B) \to \{X\} \subseteq K (\{X\})$
43	14 26 42	syl2anc	$⊢ φ \to \{X\} \subseteq K (\{X\})$
44	43 3	sseqtrrdi	$⊢ φ \to \{X\} \subseteq I$
45		snssg	$⊢ X \in B \to (X \in I \leftrightarrow \{X\} \subseteq I)$
46	45	biimpar	$⊢ (X \in B \land \{X\} \subseteq I) \to X \in I$
47	5 44 46	syl2anc	$⊢ φ \to X \in I$
48	47	adantr	$⊢ (φ \land X \in U) \to X \in I$
49	14	adantr	$⊢ (φ \land X \in U) \to R \in Ring$
50	30	adantr	$⊢ (φ \land X \in U) \to I \in LIdeal (R)$
51	4 1 41 48 49 50	lidlunitel	$⊢ (φ \land X \in U) \to I = B$
52	40 51	impbida	$⊢ φ \to (I = B \leftrightarrow X \in U)$

Metamath Proof Explorer

Theorem unitpidl1

Proof