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={\mathrm{Base}}_R$$
	pidlnzb.2	$$⊢\underset{\dot{}}{0}=0_R$$
	pidlnzb.3	$$⊢K=\mathrm{RSpan}\left(R\right)$$
Assertion	pidlnzb	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X\ne \underset{\dot{}}{0}\leftrightarrow K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pidlnzb.1	$$⊢B={\mathrm{Base}}_R$$
2		pidlnzb.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		pidlnzb.3	$$⊢K=\mathrm{RSpan}\left(R\right)$$
4	1 2 3	pidlnz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
5	4	3expa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge X\ne \underset{\dot{}}{0}\right)\to K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
6		sneq	$$⊢X=\underset{\dot{}}{0}\to \left\{X\right\}=\left\{\underset{\dot{}}{0}\right\}$$
7	6	fveq2d	$$⊢X=\underset{\dot{}}{0}\to K\left(\left\{X\right\}\right)=K\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
8	7	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge X=\underset{\dot{}}{0}\right)\to K\left(\left\{X\right\}\right)=K\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
9	3 2	rsp0	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
10	9	ad2antrr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge X=\underset{\dot{}}{0}\right)\to K\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
11	8 10	eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge X=\underset{\dot{}}{0}\right)\to K\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
12	11	ex	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X=\underset{\dot{}}{0}\to K\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
13	12	necon3d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\to X\ne \underset{\dot{}}{0}\right)$$
14	13	imp	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
15	5 14	impbida	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X\ne \underset{\dot{}}{0}\leftrightarrow K\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$