Theorem idl0cl

Description: An ideal contains 0 . (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	idl0cl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	idl0cl.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	idl0cl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝑍 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		idl0cl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		idl0cl.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
3		eqid	⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
4		eqid	⊢ ran 𝐺 = ran 𝐺
5	1 3 4 2	isidl	⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ran 𝐺 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) ) )
6	5	biimpa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ⊆ ran 𝐺 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) )
7	6	simp2d	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝑍 ∈ 𝐼 )