Definition df-lpidl 19243

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.)

Assertion

Ref	Expression
df-lpidl	|- LPIdeal = ( w e. Ring |-> U_ g e. ( Base ` w ) { ( (RSpan ` w ) ` { g } ) } )

Distinct variable group:   w, g

Detailed syntax breakdown of Definition df-lpidl

Step	Hyp	Ref	Expression
1		clpidl 19241	. 2 class LPIdeal
2		vw	. . 3 setvar w
3		crg 18547	. . 3 class Ring
4		vg	. . . 4 setvar g
5	2	cv 1482	. . . . 5 class w
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` w )
8	4	cv 1482	. . . . . . 7 class g
9	8	csn 4177	. . . . . 6 class { g }
10		crsp 19171	. . . . . . 7 class RSpan
11	5, 10	cfv 5888	. . . . . 6 class (RSpan ` w )
12	9, 11	cfv 5888	. . . . 5 class ( (RSpan ` w ) ` { g } )
13	12	csn 4177	. . . 4 class { ( (RSpan ` w ) ` { g } ) }
14	4, 7, 13	ciun 4520	. . 3 class U_ g e. ( Base ` w ) { ( (RSpan ` w ) ` { g } ) }
15	2, 3, 14	cmpt 4729	. 2 class ( w e. Ring |-> U_ g e. ( Base ` w ) { ( (RSpan ` w ) ` { g } ) } )
16	1, 15	wceq 1483	1 wff LPIdeal = ( w e. Ring |-> U_ g e. ( Base ` w ) { ( (RSpan ` w ) ` { g } ) } )

This definition is referenced by:  lpival  19245