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

Metamath Proof Explorer

Theorem lidl0ALT

Description: Alternate proof for lidl0 not using rnglidl0 : Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
rnglidl0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion lidl0ALT ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 rnglidl0.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
4 rlm0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
5 2 4 eqtri ⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
6 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
7 5 6 lsssn0 ⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → { 0 } ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
8 3 7 syl ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
9 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10 1 9 eqtri ⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11 8 10 eleqtrrdi ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )