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

Proof

Step	Hyp	Ref	Expression
1		pidlnz.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		pidlnz.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		pidlnz.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑅 ∈ Ring )
5		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑋 ∈ 𝐵 )
6	1 3	rspsnid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) )
7	4 5 6	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) )
8		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → ( 𝐾 ‘ { 𝑋 } ) = { 0 } )
9	7 8	eleqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑋 ∈ { 0 } )
10		elsni	⊢ ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
11	9 10	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑋 = 0 )
12		simpl3	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → 𝑋 ≠ 0 )
13	12	neneqd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝐾 ‘ { 𝑋 } ) = { 0 } ) → ¬ 𝑋 = 0 )
14	11 13	pm2.65da	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ¬ ( 𝐾 ‘ { 𝑋 } ) = { 0 } )
15	14	neqned	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐾 ‘ { 𝑋 } ) ≠ { 0 } )