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

Metamath Proof Explorer

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 ) )