Step |
Hyp |
Ref |
Expression |
1 |
|
dvafvsca.h |
|- H = ( LHyp ` K ) |
2 |
|
dvafvsca.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
dvafvsca.e |
|- E = ( ( TEndo ` K ) ` W ) |
4 |
|
dvafvsca.u |
|- U = ( ( DVecA ` K ) ` W ) |
5 |
|
dvafvsca.s |
|- .x. = ( .s ` U ) |
6 |
1 2 3 4 5
|
dvafvsca |
|- ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , f e. T |-> ( s ` f ) ) ) |
7 |
6
|
oveqd |
|- ( ( K e. V /\ W e. H ) -> ( R .x. F ) = ( R ( s e. E , f e. T |-> ( s ` f ) ) F ) ) |
8 |
|
fveq1 |
|- ( s = R -> ( s ` f ) = ( R ` f ) ) |
9 |
|
fveq2 |
|- ( f = F -> ( R ` f ) = ( R ` F ) ) |
10 |
|
eqid |
|- ( s e. E , f e. T |-> ( s ` f ) ) = ( s e. E , f e. T |-> ( s ` f ) ) |
11 |
|
fvex |
|- ( R ` F ) e. _V |
12 |
8 9 10 11
|
ovmpo |
|- ( ( R e. E /\ F e. T ) -> ( R ( s e. E , f e. T |-> ( s ` f ) ) F ) = ( R ` F ) ) |
13 |
7 12
|
sylan9eq |
|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T ) ) -> ( R .x. F ) = ( R ` F ) ) |