This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 elrspsn ⊢ ( ( 𝑅 ∈ 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 ⊢ ( 𝜑 → ( 𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈 ) )