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

Metamath Proof Explorer

Theorem pidlnzb

Description: A principal ideal is nonzero iff it is generated by a nonzero elements (Contributed by Thierry Arnoux, 22-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 pidlnzb.1 
 |-  B = ( Base ` R )
2 pidlnzb.2 
 |-  .0. = ( 0g ` R )
3 pidlnzb.3 
 |-  K = ( RSpan ` R )
4 1 2 3 pidlnz 
 |-  ( ( R e. Ring /\ X e. B /\ X =/= .0. ) -> ( K ` { X } ) =/= { .0. } )
5 4 3expa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ X =/= .0. ) -> ( K ` { X } ) =/= { .0. } )
6 sneq 
 |-  ( X = .0. -> { X } = { .0. } )
7 6 fveq2d 
 |-  ( X = .0. -> ( K ` { X } ) = ( K ` { .0. } ) )
8 7 adantl 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ X = .0. ) -> ( K ` { X } ) = ( K ` { .0. } ) )
9 3 2 rsp0 
 |-  ( R e. Ring -> ( K ` { .0. } ) = { .0. } )
10 9 ad2antrr 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ X = .0. ) -> ( K ` { .0. } ) = { .0. } )
11 8 10 eqtrd 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ X = .0. ) -> ( K ` { X } ) = { .0. } )
12 11 ex 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X = .0. -> ( K ` { X } ) = { .0. } ) )
13 12 necon3d 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( K ` { X } ) =/= { .0. } -> X =/= .0. ) )
14 13 imp 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ ( K ` { X } ) =/= { .0. } ) -> X =/= .0. )
15 5 14 impbida 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X =/= .0. <-> ( K ` { X } ) =/= { .0. } ) )