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

Metamath Proof Explorer

Theorem lidlnz

Description: A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlnz.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidlnz.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion lidlnz ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃ 𝑥 ∈ 𝐼 𝑥 ≠ 0 )

Proof

Step Hyp Ref Expression
1 lidlnz.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidlnz.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 1 2 lidl0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )
4 3 snssd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → { 0 } ⊆ 𝐼 )
5 4 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → { 0 } ⊆ 𝐼 )
6 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ≠ { 0 } )
7 6 necomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → { 0 } ≠ 𝐼 )
8 df-pss ⊢ ( { 0 } ⊊ 𝐼 ↔ ( { 0 } ⊆ 𝐼 ∧ { 0 } ≠ 𝐼 ) )
9 5 7 8 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → { 0 } ⊊ 𝐼 )
10 pssnel ⊢ ( { 0 } ⊊ 𝐼 → ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ { 0 } ) )
11 9 10 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ { 0 } ) )
12 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
13 12 necon3bbii ⊢ ( ¬ 𝑥 ∈ { 0 } ↔ 𝑥 ≠ 0 )
14 13 anbi2i ⊢ ( ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ { 0 } ) ↔ ( 𝑥 ∈ 𝐼 ∧ 𝑥 ≠ 0 ) )
15 14 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ { 0 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ 𝑥 ≠ 0 ) )
16 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐼 𝑥 ≠ 0 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ 𝑥 ≠ 0 ) )
17 15 16 bitr4i ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ { 0 } ) ↔ ∃ 𝑥 ∈ 𝐼 𝑥 ≠ 0 )
18 11 17 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃ 𝑥 ∈ 𝐼 𝑥 ≠ 0 )