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