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