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

Metamath Proof Explorer

Theorem lidlnegcl

Description: An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidlnegcl.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion lidlnegcl ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidlnegcl.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
3 rlmvneg ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ ( ringLMod ‘ 𝑅 ) )
4 2 3 eqtri ⊢ 𝑁 = ( invg ‘ ( ringLMod ‘ 𝑅 ) )
5 4 fveq1i ⊢ ( 𝑁 ‘ 𝑋 ) = ( ( invg ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑋 )
6 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
7 6 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
8 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
9 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10 1 9 eqtri ⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11 8 10 eleqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
12 11 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
13 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ∈ 𝐼 )
14 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
15 eqid ⊢ ( invg ‘ ( ringLMod ‘ 𝑅 ) ) = ( invg ‘ ( ringLMod ‘ 𝑅 ) )
16 14 15 lssvnegcl ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ∧ 𝑋 ∈ 𝐼 ) → ( ( invg ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑋 ) ∈ 𝐼 )
17 7 12 13 16 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( ( invg ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑋 ) ∈ 𝐼 )
18 5 17 eqeltrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )