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 
|- U = ( Unit ` R )
unitpidl1.2 
|- K = ( RSpan ` R )
unitpidl1.3 
|- I = ( K ` { X } )
unitpidl1.4 
|- B = ( Base ` R )
unitpidl1.5 
|- ( ph -> X e. B )
unitpidl1.6 
|- ( ph -> R e. IDomn )
Assertion unitpidl1 
|- ( ph -> ( I = B <-> X e. 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 
 |-  ( ph -> X e. B )
6 unitpidl1.6 
 |-  ( ph -> R e. IDomn )
7 df-idom 
 |-  IDomn = ( CRing i^i Domn )
8 6 7 eleqtrdi 
 |-  ( ph -> R e. ( CRing i^i Domn ) )
9 8 elin1d 
 |-  ( ph -> R e. CRing )
10 9 ad3antrrr 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> R e. CRing )
11 simplr 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> y e. B )
12 5 ad3antrrr 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> X e. B )
13 simpr 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> ( 1r ` R ) = ( y ( .r ` R ) X ) )
14 6 idomringd 
 |-  ( ph -> R e. Ring )
15 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 1 15 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
17 14 16 syl 
 |-  ( ph -> ( 1r ` R ) e. U )
18 17 ad3antrrr 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> ( 1r ` R ) e. U )
19 13 18 eqeltrrd 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> ( y ( .r ` R ) X ) e. U )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 1 20 4 unitmulclb 
 |-  ( ( R e. CRing /\ y e. B /\ X e. B ) -> ( ( y ( .r ` R ) X ) e. U <-> ( y e. U /\ X e. U ) ) )
22 21 simplbda 
 |-  ( ( ( R e. CRing /\ y e. B /\ X e. B ) /\ ( y ( .r ` R ) X ) e. U ) -> X e. U )
23 10 11 12 19 22 syl31anc 
 |-  ( ( ( ( ph /\ I = B ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) X ) ) -> X e. U )
24 14 adantr 
 |-  ( ( ph /\ I = B ) -> R e. Ring )
25 5 adantr 
 |-  ( ( ph /\ I = B ) -> X e. B )
26 5 snssd 
 |-  ( ph -> { X } C_ B )
27 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
28 2 4 27 rspcl 
 |-  ( ( R e. Ring /\ { X } C_ B ) -> ( K ` { X } ) e. ( LIdeal ` R ) )
29 14 26 28 syl2anc 
 |-  ( ph -> ( K ` { X } ) e. ( LIdeal ` R ) )
30 3 29 eqeltrid 
 |-  ( ph -> I e. ( LIdeal ` R ) )
31 30 adantr 
 |-  ( ( ph /\ I = B ) -> I e. ( LIdeal ` R ) )
32 simpr 
 |-  ( ( ph /\ I = B ) -> I = B )
33 27 4 15 lidl1el 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> ( ( 1r ` R ) e. I <-> I = B ) )
34 33 biimpar 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I = B ) -> ( 1r ` R ) e. I )
35 24 31 32 34 syl21anc 
 |-  ( ( ph /\ I = B ) -> ( 1r ` R ) e. I )
36 35 3 eleqtrdi 
 |-  ( ( ph /\ I = B ) -> ( 1r ` R ) e. ( K ` { X } ) )
37 4 20 2 rspsnel 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 1r ` R ) e. ( K ` { X } ) <-> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) X ) ) )
38 37 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ ( 1r ` R ) e. ( K ` { X } ) ) -> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) X ) )
39 24 25 36 38 syl21anc 
 |-  ( ( ph /\ I = B ) -> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) X ) )
40 23 39 r19.29a 
 |-  ( ( ph /\ I = B ) -> X e. U )
41 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
42 2 4 rspssid 
 |-  ( ( R e. Ring /\ { X } C_ B ) -> { X } C_ ( K ` { X } ) )
43 14 26 42 syl2anc 
 |-  ( ph -> { X } C_ ( K ` { X } ) )
44 43 3 sseqtrrdi 
 |-  ( ph -> { X } C_ I )
45 snssg 
 |-  ( X e. B -> ( X e. I <-> { X } C_ I ) )
46 45 biimpar 
 |-  ( ( X e. B /\ { X } C_ I ) -> X e. I )
47 5 44 46 syl2anc 
 |-  ( ph -> X e. I )
48 47 adantr 
 |-  ( ( ph /\ X e. U ) -> X e. I )
49 14 adantr 
 |-  ( ( ph /\ X e. U ) -> R e. Ring )
50 30 adantr 
 |-  ( ( ph /\ X e. U ) -> I e. ( LIdeal ` R ) )
51 4 1 41 48 49 50 lidlunitel 
 |-  ( ( ph /\ X e. U ) -> I = B )
52 40 51 impbida 
 |-  ( ph -> ( I = B <-> X e. U ) )