Metamath Proof Explorer

Theorem pidlnz

Description: A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024)

Ref Expression
Hypotheses pidlnz.1 
|- B = ( Base ` R )
pidlnz.2 
|- .0. = ( 0g ` R )
pidlnz.3 
|- K = ( RSpan ` R )
Assertion pidlnz 
|- ( ( R e. Ring /\ X e. B /\ X =/= .0. ) -> ( K ` { X } ) =/= { .0. } )

Proof

Step Hyp Ref Expression
1 pidlnz.1 
 |-  B = ( Base ` R )
2 pidlnz.2 
 |-  .0. = ( 0g ` R )
3 pidlnz.3 
 |-  K = ( RSpan ` R )
4 simpl1 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> R e. Ring )
5 simpl2 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> X e. B )
6 1 3 rspsnid 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. ( K ` { X } ) )
7 4 5 6 syl2anc 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> X e. ( K ` { X } ) )
8 simpr 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> ( K ` { X } ) = { .0. } )
9 7 8 eleqtrd 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> X e. { .0. } )
10 elsni 
 |-  ( X e. { .0. } -> X = .0. )
11 9 10 syl 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> X = .0. )
12 simpl3 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> X =/= .0. )
13 12 neneqd 
 |-  ( ( ( R e. Ring /\ X e. B /\ X =/= .0. ) /\ ( K ` { X } ) = { .0. } ) -> -. X = .0. )
14 11 13 pm2.65da 
 |-  ( ( R e. Ring /\ X e. B /\ X =/= .0. ) -> -. ( K ` { X } ) = { .0. } )
15 14 neqned 
 |-  ( ( R e. Ring /\ X e. B /\ X =/= .0. ) -> ( K ` { X } ) =/= { .0. } )