islidl

Description: Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	islidl.s	$⊢ U = LIdeal (R)$
	islidl.b	$⊢ B = {Base}_{R}$
	islidl.p	$⊢ \underset{˙}{+} = +_{R}$
	islidl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	islidl	$⊢ I \in U \leftrightarrow (I \subseteq B \land I \neq \emptyset \land \forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) \underset{˙}{+} b \in I)$

Step	Hyp	Ref	Expression
1		islidl.s	$⊢ U = LIdeal (R)$
2		islidl.b	$⊢ B = {Base}_{R}$
3		islidl.p	$⊢ \underset{˙}{+} = +_{R}$
4		islidl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		rlmsca2	$⊢ I (R) = Scalar (ringLMod (R))$
6		baseid	$⊢ Base = Slot {Base}_{ndx}$
7	6 2	strfvi	$⊢ B = {Base}_{I (R)}$
8		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
9	2 8	eqtri	$⊢ B = {Base}_{ringLMod (R)}$
10		rlmplusg	$⊢ +_{R} = +_{ringLMod (R)}$
11	3 10	eqtri	$⊢ \underset{˙}{+} = +_{ringLMod (R)}$
12		rlmvsca	$⊢ \cdot_{R} = \cdot_{ringLMod (R)}$
13	4 12	eqtri	$⊢ \underset{˙}{\cdot} = \cdot_{ringLMod (R)}$
14		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
15	1 14	eqtri	$⊢ U = LSubSp (ringLMod (R))$
16	5 7 9 11 13 15	islss	$⊢ I \in U \leftrightarrow (I \subseteq B \land I \neq \emptyset \land \forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) \underset{˙}{+} b \in I)$

Metamath Proof Explorer