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

Metamath Proof Explorer

Definition df-lpidl

Description: Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Assertion df-lpidl LPIdeal = ( 𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ ( Base ‘ 𝑤 ) { ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpidl ⊢ LPIdeal
1 vw ⊢ 𝑤
2 crg ⊢ Ring
3 vg ⊢ 𝑔
4 cbs ⊢ Base
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( Base ‘ 𝑤 )
7 crsp ⊢ RSpan
8 5 7 cfv ⊢ ( RSpan ‘ 𝑤 )
9 3 cv ⊢ 𝑔
10 9 csn ⊢ { 𝑔 }
11 10 8 cfv ⊢ ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } )
12 11 csn ⊢ { ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } ) }
13 3 6 12 ciun ⊢ ∪ 𝑔 ∈ ( Base ‘ 𝑤 ) { ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } ) }
14 1 2 13 cmpt ⊢ ( 𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ ( Base ‘ 𝑤 ) { ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } ) } )
15 0 14 wceq ⊢ LPIdeal = ( 𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ ( Base ‘ 𝑤 ) { ( ( RSpan ‘ 𝑤 ) ‘ { 𝑔 } ) } )