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	$⊢ \underset{˙}{0} = 0_{R}$
	pidlnzb.3	$⊢ K = RSpan (R)$
Assertion	pidlnzb	$⊢ (R \in Ring \land X \in B) \to (X \neq \underset{˙}{0} \leftrightarrow K (\{X\}) \neq \{\underset{˙}{0}\})$

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

Metamath Proof Explorer