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 ‘ 𝑤 ) ‘ { 𝑔 } ) } )