This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )