Theorem islidl

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

	Ref	Expression
Hypotheses	islidl.s	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
	islidl.b	$$⊢B={\mathrm{Base}}_R$$
	islidl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	islidl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	islidl	$$⊢I\in U\leftrightarrow \left(I\subseteq B\wedge I\ne \varnothing \wedge \forall x\in B\forall a\in I\forall b\in I\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in I\right)$$

Proof

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