Theorem 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	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitpidl1.2	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	unitpidl1.3	⊢ 𝐼 = ( 𝐾 ‘ { 𝑋 } )
	unitpidl1.4	⊢ 𝐵 = ( Base ‘ 𝑅 )
	unitpidl1.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	unitpidl1.6	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion	unitpidl1	⊢ ( 𝜑 → ( 𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		unitpidl1.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitpidl1.2	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		unitpidl1.3	⊢ 𝐼 = ( 𝐾 ‘ { 𝑋 } )
4		unitpidl1.4	⊢ 𝐵 = ( Base ‘ 𝑅 )
5		unitpidl1.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		unitpidl1.6	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
7		df-idom	⊢ IDomn = ( CRing ∩ Domn )
8	6 7	eleqtrdi	⊢ ( 𝜑 → 𝑅 ∈ ( CRing ∩ Domn ) )
9	8	elin1d	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ CRing )
11		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑦 ∈ 𝐵 )
12	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑋 ∈ 𝐵 )
13		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
14	6	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16	1 15	1unit	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
17	14 16	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
18	17	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
19	13 18	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝑈 )
20		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21	1 20 4	unitmulclb	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝑈 ↔ ( 𝑦 ∈ 𝑈 ∧ 𝑋 ∈ 𝑈 ) ) )
22	21	simplbda	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
23	10 11 12 19 22	syl31anc	⊢ ( ( ( ( 𝜑 ∧ 𝐼 = 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑋 ∈ 𝑈 )
24	14	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → 𝑅 ∈ Ring )
25	5	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → 𝑋 ∈ 𝐵 )
26	5	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
27		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
28	2 4 27	rspcl	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
29	14 26 28	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
30	3 29	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → 𝐼 = 𝐵 )
33	27 4 15	lidl1el	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )
34	33	biimpar	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 = 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐼 )
35	24 31 32 34	syl21anc	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐼 )
36	35 3	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑋 } ) )
37	4 20 2	rspsnel	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
38	37	biimpa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
39	24 25 36 38	syl21anc	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
40	23 39	r19.29a	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐵 ) → 𝑋 ∈ 𝑈 )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
42	2 4	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
43	14 26 42	syl2anc	⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
44	43 3	sseqtrrdi	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
45		snssg	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝐼 ↔ { 𝑋 } ⊆ 𝐼 ) )
46	45	biimpar	⊢ ( ( 𝑋 ∈ 𝐵 ∧ { 𝑋 } ⊆ 𝐼 ) → 𝑋 ∈ 𝐼 )
47	5 44 46	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝐼 )
49	14	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ Ring )
50	30	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
51	4 1 41 48 49 50	lidlunitel	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐼 = 𝐵 )
52	40 51	impbida	⊢ ( 𝜑 → ( 𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈 ) )