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