Step |
Hyp |
Ref |
Expression |
1 |
|
lflf.d |
|- D = ( Scalar ` W ) |
2 |
|
lflf.k |
|- K = ( Base ` D ) |
3 |
|
lflf.v |
|- V = ( Base ` W ) |
4 |
|
lflf.f |
|- F = ( LFnl ` W ) |
5 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
6 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
7 |
|
eqid |
|- ( +g ` D ) = ( +g ` D ) |
8 |
|
eqid |
|- ( .r ` D ) = ( .r ` D ) |
9 |
3 5 1 6 2 7 8 4
|
islfl |
|- ( W e. X -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( G ` x ) ) ( +g ` D ) ( G ` y ) ) ) ) ) |
10 |
9
|
simprbda |
|- ( ( W e. X /\ G e. F ) -> G : V --> K ) |