This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in Ring ⟼ ⋃_{g \in {Base}_{w}} \{RSpan (w) (\{g\})\})$

Detailed syntax breakdown

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