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 = ( w e. Ring |-> U_ g e. ( Base ` w ) { ( ( RSpan ` w ) ` { g } ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpidl	|- LPIdeal
1		vw	|- w
2		crg	|- Ring
3		vg	|- g
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7		crsp	|- RSpan
8	5 7	cfv	|- ( RSpan ` w )
9	3	cv	|- g
10	9	csn	|- { g }
11	10 8	cfv	|- ( ( RSpan ` w ) ` { g } )
12	11	csn	|- { ( ( RSpan ` w ) ` { g } ) }
13	3 6 12	ciun	|- U_ g e. ( Base ` w ) { ( ( RSpan ` w ) ` { g } ) }
14	1 2 13	cmpt	|- ( w e. Ring |-> U_ g e. ( Base ` w ) { ( ( RSpan ` w ) ` { g } ) } )
15	0 14	wceq	|- LPIdeal = ( w e. Ring |-> U_ g e. ( Base ` w ) { ( ( RSpan ` w ) ` { g } ) } )