Theorem islpidl

Description: Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpival.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	lpival.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	islpidl	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2		lpival.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		lpival.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4	1 2 3	lpival	⊢ ( 𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } )
5	4	eleq2d	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑃 ↔ 𝐼 ∈ ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } ) )
6		eliun	⊢ ( 𝐼 ∈ ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } ↔ ∃ 𝑔 ∈ 𝐵 𝐼 ∈ { ( 𝐾 ‘ { 𝑔 } ) } )
7		fvex	⊢ ( 𝐾 ‘ { 𝑔 } ) ∈ V
8	7	elsn2	⊢ ( 𝐼 ∈ { ( 𝐾 ‘ { 𝑔 } ) } ↔ 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )
9	8	rexbii	⊢ ( ∃ 𝑔 ∈ 𝐵 𝐼 ∈ { ( 𝐾 ‘ { 𝑔 } ) } ↔ ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )
10	6 9	bitri	⊢ ( 𝐼 ∈ ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } ↔ ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )
11	5 10	bitrdi	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) ) )