Step |
Hyp |
Ref |
Expression |
1 |
|
dvafvadd.h |
|- H = ( LHyp ` K ) |
2 |
|
dvafvadd.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
dvafvadd.u |
|- U = ( ( DVecA ` K ) ` W ) |
4 |
|
dvafvadd.v |
|- .+ = ( +g ` U ) |
5 |
1 2 3 4
|
dvafvadd |
|- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) ) |
6 |
5
|
oveqd |
|- ( ( K e. V /\ W e. H ) -> ( F .+ G ) = ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) ) |
7 |
|
coexg |
|- ( ( F e. T /\ G e. T ) -> ( F o. G ) e. _V ) |
8 |
|
coeq1 |
|- ( f = F -> ( f o. g ) = ( F o. g ) ) |
9 |
|
coeq2 |
|- ( g = G -> ( F o. g ) = ( F o. G ) ) |
10 |
|
eqid |
|- ( f e. T , g e. T |-> ( f o. g ) ) = ( f e. T , g e. T |-> ( f o. g ) ) |
11 |
8 9 10
|
ovmpog |
|- ( ( F e. T /\ G e. T /\ ( F o. G ) e. _V ) -> ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) = ( F o. G ) ) |
12 |
7 11
|
mpd3an3 |
|- ( ( F e. T /\ G e. T ) -> ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) = ( F o. G ) ) |
13 |
6 12
|
sylan9eq |
|- ( ( ( K e. V /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( F .+ G ) = ( F o. G ) ) |