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

Proof

Step	Hyp	Ref	Expression
1		pidlnz.1	$⊢ B = {Base}_{R}$
2		pidlnz.2	$⊢ \underset{˙}{0} = 0_{R}$
3		pidlnz.3	$⊢ K = RSpan (R)$
4		simpl1	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to R \in Ring$
5		simpl2	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to X \in B$
6	1 3	rspsnid	$⊢ (R \in Ring \land X \in B) \to X \in K (\{X\})$
7	4 5 6	syl2anc	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to X \in K (\{X\})$
8		simpr	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to K (\{X\}) = \{\underset{˙}{0}\}$
9	7 8	eleqtrd	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to X \in \{\underset{˙}{0}\}$
10		elsni	$⊢ X \in \{\underset{˙}{0}\} \to X = \underset{˙}{0}$
11	9 10	syl	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to X = \underset{˙}{0}$
12		simpl3	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
13	12	neneqd	$⊢ ((R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \land K (\{X\}) = \{\underset{˙}{0}\}) \to \neg X = \underset{˙}{0}$
14	11 13	pm2.65da	$⊢ (R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \to \neg K (\{X\}) = \{\underset{˙}{0}\}$
15	14	neqned	$⊢ (R \in Ring \land X \in B \land X \neq \underset{˙}{0}) \to K (\{X\}) \neq \{\underset{˙}{0}\}$