Definition df-lpidl 20427

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 = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})

Distinct variable group:   𝑤,𝑔

Detailed syntax breakdown of Definition df-lpidl

Step	Hyp	Ref	Expression
1		clpidl 20425	. 2 class LPIdeal
2		vw	. . 3 setvar 𝑤
3		crg 19698	. . 3 class Ring
4		vg	. . . 4 setvar 𝑔
5	2	cv 1538	. . . . 5 class 𝑤
6		cbs 16840	. . . . 5 class Base
7	5, 6	cfv 6418	. . . 4 class (Base‘𝑤)
8	4	cv 1538	. . . . . . 7 class 𝑔
9	8	csn 4558	. . . . . 6 class {𝑔}
10		crsp 20348	. . . . . . 7 class RSpan
11	5, 10	cfv 6418	. . . . . 6 class (RSpan‘𝑤)
12	9, 11	cfv 6418	. . . . 5 class ((RSpan‘𝑤)‘{𝑔})
13	12	csn 4558	. . . 4 class {((RSpan‘𝑤)‘{𝑔})}
14	4, 7, 13	ciun 4921	. . 3 class ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})}
15	2, 3, 14	cmpt 5153	. 2 class (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
16	1, 15	wceq 1539	1 wff LPIdeal = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})

This definition is referenced by:  lpival  20429