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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pidlnzb.2	⊢ 0 = ( 0g ‘ 𝑅 )
	pidlnzb.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion	pidlnzb	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≠ 0 ↔ ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		pidlnzb.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		pidlnzb.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		pidlnzb.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4	1 2 3	pidlnz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } )
5	4	3expa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ≠ 0 ) → ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } )
6		sneq	⊢ ( 𝑋 = 0 → { 𝑋 } = { 0 } )
7	6	fveq2d	⊢ ( 𝑋 = 0 → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 0 } ) )
8	7	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 = 0 ) → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 0 } ) )
9	3 2	rsp0	⊢ ( 𝑅 ∈ Ring → ( 𝐾 ‘ { 0 } ) = { 0 } )
10	9	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 = 0 ) → ( 𝐾 ‘ { 0 } ) = { 0 } )
11	8 10	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 = 0 ) → ( 𝐾 ‘ { 𝑋 } ) = { 0 } )
12	11	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 = 0 → ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) )
13	12	necon3d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } → 𝑋 ≠ 0 ) )
14	13	imp	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } ) → 𝑋 ≠ 0 )
15	5 14	impbida	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≠ 0 ↔ ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } ) )