| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lflass.v |
|- V = ( Base ` W ) |
| 2 |
|
lflass.r |
|- R = ( Scalar ` W ) |
| 3 |
|
lflass.k |
|- K = ( Base ` R ) |
| 4 |
|
lflass.t |
|- .x. = ( .r ` R ) |
| 5 |
|
lflass.f |
|- F = ( LFnl ` W ) |
| 6 |
|
lflass.w |
|- ( ph -> W e. LMod ) |
| 7 |
|
lflass.x |
|- ( ph -> X e. K ) |
| 8 |
|
lflass.y |
|- ( ph -> Y e. K ) |
| 9 |
|
lflass.g |
|- ( ph -> G e. F ) |
| 10 |
1
|
fvexi |
|- V e. _V |
| 11 |
10
|
a1i |
|- ( ph -> V e. _V ) |
| 12 |
2 3 1 5
|
lflf |
|- ( ( W e. LMod /\ G e. F ) -> G : V --> K ) |
| 13 |
6 9 12
|
syl2anc |
|- ( ph -> G : V --> K ) |
| 14 |
|
fconst6g |
|- ( X e. K -> ( V X. { X } ) : V --> K ) |
| 15 |
7 14
|
syl |
|- ( ph -> ( V X. { X } ) : V --> K ) |
| 16 |
|
fconst6g |
|- ( Y e. K -> ( V X. { Y } ) : V --> K ) |
| 17 |
8 16
|
syl |
|- ( ph -> ( V X. { Y } ) : V --> K ) |
| 18 |
2
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
| 19 |
6 18
|
syl |
|- ( ph -> R e. Ring ) |
| 20 |
3 4
|
ringass |
|- ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) |
| 21 |
19 20
|
sylan |
|- ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) |
| 22 |
11 13 15 17 21
|
caofass |
|- ( ph -> ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) = ( G oF .x. ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) ) ) |
| 23 |
11 7 8
|
ofc12 |
|- ( ph -> ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) = ( V X. { ( X .x. Y ) } ) ) |
| 24 |
23
|
oveq2d |
|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) ) = ( G oF .x. ( V X. { ( X .x. Y ) } ) ) ) |
| 25 |
22 24
|
eqtr2d |
|- ( ph -> ( G oF .x. ( V X. { ( X .x. Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) ) |