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

Metamath Proof Explorer

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 → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) ) )