Metamath Proof Explorer


Theorem islidl

Description: Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses islidl.s 𝑈 = ( LIdeal ‘ 𝑅 )
islidl.b 𝐵 = ( Base ‘ 𝑅 )
islidl.p + = ( +g𝑅 )
islidl.t · = ( .r𝑅 )
Assertion islidl ( 𝐼𝑈 ↔ ( 𝐼𝐵𝐼 ≠ ∅ ∧ ∀ 𝑥𝐵𝑎𝐼𝑏𝐼 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 islidl.s 𝑈 = ( LIdeal ‘ 𝑅 )
2 islidl.b 𝐵 = ( Base ‘ 𝑅 )
3 islidl.p + = ( +g𝑅 )
4 islidl.t · = ( .r𝑅 )
5 rlmsca2 ( I ‘ 𝑅 ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
6 baseid Base = Slot ( Base ‘ ndx )
7 6 2 strfvi 𝐵 = ( Base ‘ ( I ‘ 𝑅 ) )
8 rlmbas ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
9 2 8 eqtri 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
10 rlmplusg ( +g𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
11 3 10 eqtri + = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
12 rlmvsca ( .r𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
13 4 12 eqtri · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
14 lidlval ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
15 1 14 eqtri 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
16 5 7 9 11 13 15 islss ( 𝐼𝑈 ↔ ( 𝐼𝐵𝐼 ≠ ∅ ∧ ∀ 𝑥𝐵𝑎𝐼𝑏𝐼 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝐼 ) )