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	$$⊢\mathrm{LPIdeal}=\left(w\in \mathrm{Ring}⟼\bigcup _{g\in {\mathrm{Base}}_w}\left\{\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpidl	$$class\mathrm{LPIdeal}$$
1		vw	$$setvarw$$
2		crg	$$class\mathrm{Ring}$$
3		vg	$$setvarg$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7		crsp	$$class\mathrm{RSpan}$$
8	5 7	cfv	$$class\mathrm{RSpan}\left(w\right)$$
9	3	cv	$$setvarg$$
10	9	csn	$$class\left\{g\right\}$$
11	10 8	cfv	$$class\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)$$
12	11	csn	$$class\left\{\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)\right\}$$
13	3 6 12	ciun	$$class\bigcup _{g\in {\mathrm{Base}}_w}\left\{\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)\right\}$$
14	1 2 13	cmpt	$$class\left(w\in \mathrm{Ring}⟼\bigcup _{g\in {\mathrm{Base}}_w}\left\{\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{LPIdeal}=\left(w\in \mathrm{Ring}⟼\bigcup _{g\in {\mathrm{Base}}_w}\left\{\mathrm{RSpan}\left(w\right)\left(\left\{g\right\}\right)\right\}\right)$$