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 )