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