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. } ) )