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

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 → 𝑃 ⊆ 𝑈 )