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