unitpidl1

Description: The ideal I generated by an element X of a commutative ring 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 CRing$
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 CRing$
7	6	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to R \in CRing$
8		simplr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to y \in B$
9	5	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to X \in B$
10		simpr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to 1_{R} = y \cdot_{R} X$
11	6	crngringd	$⊢ φ \to R \in Ring$
12		eqid	$⊢ 1_{R} = 1_{R}$
13	1 12	1unit	$⊢ R \in Ring \to 1_{R} \in U$
14	11 13	syl	$⊢ φ \to 1_{R} \in U$
15	14	ad3antrrr	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to 1_{R} \in U$
16	10 15	eqeltrrd	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to y \cdot_{R} X \in U$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	1 17 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))$
19	18	simplbda	$⊢ ((R \in CRing \land y \in B \land X \in B) \land y \cdot_{R} X \in U) \to X \in U$
20	7 8 9 16 19	syl31anc	$⊢ (((φ \land I = B) \land y \in B) \land 1_{R} = y \cdot_{R} X) \to X \in U$
21	11	adantr	$⊢ (φ \land I = B) \to R \in Ring$
22	5	adantr	$⊢ (φ \land I = B) \to X \in B$
23	5	snssd	$⊢ φ \to \{X\} \subseteq B$
24		eqid	$⊢ LIdeal (R) = LIdeal (R)$
25	2 4 24	rspcl	$⊢ (R \in Ring \land \{X\} \subseteq B) \to K (\{X\}) \in LIdeal (R)$
26	11 23 25	syl2anc	$⊢ φ \to K (\{X\}) \in LIdeal (R)$
27	3 26	eqeltrid	$⊢ φ \to I \in LIdeal (R)$
28	27	adantr	$⊢ (φ \land I = B) \to I \in LIdeal (R)$
29		simpr	$⊢ (φ \land I = B) \to I = B$
30	24 4 12	lidl1el	$⊢ (R \in Ring \land I \in LIdeal (R)) \to (1_{R} \in I \leftrightarrow I = B)$
31	30	biimpar	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land I = B) \to 1_{R} \in I$
32	21 28 29 31	syl21anc	$⊢ (φ \land I = B) \to 1_{R} \in I$
33	32 3	eleqtrdi	$⊢ (φ \land I = B) \to 1_{R} \in K (\{X\})$
34	4 17 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)$
35	34	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$
36	21 22 33 35	syl21anc	$⊢ (φ \land I = B) \to \exists y \in B 1_{R} = y \cdot_{R} X$
37	20 36	r19.29a	$⊢ (φ \land I = B) \to X \in U$
38		simpr	$⊢ (φ \land X \in U) \to X \in U$
39	2 4	rspssid	$⊢ (R \in Ring \land \{X\} \subseteq B) \to \{X\} \subseteq K (\{X\})$
40	11 23 39	syl2anc	$⊢ φ \to \{X\} \subseteq K (\{X\})$
41	40 3	sseqtrrdi	$⊢ φ \to \{X\} \subseteq I$
42		snssg	$⊢ X \in B \to (X \in I \leftrightarrow \{X\} \subseteq I)$
43	42	biimpar	$⊢ (X \in B \land \{X\} \subseteq I) \to X \in I$
44	5 41 43	syl2anc	$⊢ φ \to X \in I$
45	44	adantr	$⊢ (φ \land X \in U) \to X \in I$
46	11	adantr	$⊢ (φ \land X \in U) \to R \in Ring$
47	27	adantr	$⊢ (φ \land X \in U) \to I \in LIdeal (R)$
48	4 1 38 45 46 47	lidlunitel	$⊢ (φ \land X \in U) \to I = B$
49	37 48	impbida	$⊢ φ \to (I = B \leftrightarrow X \in U)$

Metamath Proof Explorer

Theorem unitpidl1

Proof