Step |
Hyp |
Ref |
Expression |
1 |
|
lflset.v |
|- V = ( Base ` W ) |
2 |
|
lflset.a |
|- .+ = ( +g ` W ) |
3 |
|
lflset.d |
|- D = ( Scalar ` W ) |
4 |
|
lflset.s |
|- .x. = ( .s ` W ) |
5 |
|
lflset.k |
|- K = ( Base ` D ) |
6 |
|
lflset.p |
|- .+^ = ( +g ` D ) |
7 |
|
lflset.t |
|- .X. = ( .r ` D ) |
8 |
|
lflset.f |
|- F = ( LFnl ` W ) |
9 |
1 2 3 4 5 6 7 8
|
islfl |
|- ( W e. Z -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) ) ) |
10 |
9
|
simplbda |
|- ( ( W e. Z /\ G e. F ) -> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) |
11 |
10
|
3adant3 |
|- ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) ) |
12 |
|
oveq1 |
|- ( r = R -> ( r .x. x ) = ( R .x. x ) ) |
13 |
12
|
fvoveq1d |
|- ( r = R -> ( G ` ( ( r .x. x ) .+ y ) ) = ( G ` ( ( R .x. x ) .+ y ) ) ) |
14 |
|
oveq1 |
|- ( r = R -> ( r .X. ( G ` x ) ) = ( R .X. ( G ` x ) ) ) |
15 |
14
|
oveq1d |
|- ( r = R -> ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) ) |
16 |
13 15
|
eqeq12d |
|- ( r = R -> ( ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. x ) .+ y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) ) ) |
17 |
|
oveq2 |
|- ( x = X -> ( R .x. x ) = ( R .x. X ) ) |
18 |
17
|
fvoveq1d |
|- ( x = X -> ( G ` ( ( R .x. x ) .+ y ) ) = ( G ` ( ( R .x. X ) .+ y ) ) ) |
19 |
|
fveq2 |
|- ( x = X -> ( G ` x ) = ( G ` X ) ) |
20 |
19
|
oveq2d |
|- ( x = X -> ( R .X. ( G ` x ) ) = ( R .X. ( G ` X ) ) ) |
21 |
20
|
oveq1d |
|- ( x = X -> ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) ) |
22 |
18 21
|
eqeq12d |
|- ( x = X -> ( ( G ` ( ( R .x. x ) .+ y ) ) = ( ( R .X. ( G ` x ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. X ) .+ y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) ) ) |
23 |
|
oveq2 |
|- ( y = Y -> ( ( R .x. X ) .+ y ) = ( ( R .x. X ) .+ Y ) ) |
24 |
23
|
fveq2d |
|- ( y = Y -> ( G ` ( ( R .x. X ) .+ y ) ) = ( G ` ( ( R .x. X ) .+ Y ) ) ) |
25 |
|
fveq2 |
|- ( y = Y -> ( G ` y ) = ( G ` Y ) ) |
26 |
25
|
oveq2d |
|- ( y = Y -> ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) |
27 |
24 26
|
eqeq12d |
|- ( y = Y -> ( ( G ` ( ( R .x. X ) .+ y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` y ) ) <-> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) ) |
28 |
16 22 27
|
rspc3v |
|- ( ( R e. K /\ X e. V /\ Y e. V ) -> ( A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) -> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) ) |
29 |
28
|
3ad2ant3 |
|- ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( A. r e. K A. x e. V A. y e. V ( G ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( G ` x ) ) .+^ ( G ` y ) ) -> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) ) |
30 |
11 29
|
mpd |
|- ( ( W e. Z /\ G e. F /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( G ` ( ( R .x. X ) .+ Y ) ) = ( ( R .X. ( G ` X ) ) .+^ ( G ` Y ) ) ) |