Metamath Proof Explorer


Theorem lpiss

Description: Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p 𝑃 = ( LPIdeal ‘ 𝑅 )
lpiss.u 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion lpiss ( 𝑅 ∈ Ring → 𝑃𝑈 )

Proof

Step Hyp Ref Expression
1 lpival.p 𝑃 = ( LPIdeal ‘ 𝑅 )
2 lpiss.u 𝑈 = ( LIdeal ‘ 𝑅 )
3 eqid ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 1 3 4 islpidl ( 𝑅 ∈ Ring → ( 𝑎𝑃 ↔ ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ) )
6 snssi ( 𝑔 ∈ ( Base ‘ 𝑅 ) → { 𝑔 } ⊆ ( Base ‘ 𝑅 ) )
7 3 4 2 rspcl ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 )
8 6 7 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 )
9 eleq1 ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → ( 𝑎𝑈 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ 𝑈 ) )
10 8 9 syl5ibrcom ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → 𝑎𝑈 ) )
11 10 rexlimdva ( 𝑅 ∈ Ring → ( ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) → 𝑎𝑈 ) )
12 5 11 sylbid ( 𝑅 ∈ Ring → ( 𝑎𝑃𝑎𝑈 ) )
13 12 ssrdv ( 𝑅 ∈ Ring → 𝑃𝑈 )