Theorem 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	|- .+ = ( +g ` R )
	islidl.t	|- .x. = ( .r ` R )
Assertion	islidl	|- ( I e. U <-> ( I C_ B /\ I =/= (/) /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) .+ b ) e. I ) )

Proof

Step	Hyp	Ref	Expression
1		islidl.s	|- U = ( LIdeal ` R )
2		islidl.b	|- B = ( Base ` R )
3		islidl.p	|- .+ = ( +g ` R )
4		islidl.t	|- .x. = ( .r ` 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	|- ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
11	3 10	eqtri	|- .+ = ( +g ` ( ringLMod ` R ) )
12		rlmvsca	|- ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
13	4 12	eqtri	|- .x. = ( .s ` ( 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 e. U <-> ( I C_ B /\ I =/= (/) /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) .+ b ) e. I ) )