Step |
Hyp |
Ref |
Expression |
1 |
|
dvhbase.h |
|- H = ( LHyp ` K ) |
2 |
|
dvhbase.e |
|- E = ( ( TEndo ` K ) ` W ) |
3 |
|
dvhbase.u |
|- U = ( ( DVecH ` K ) ` W ) |
4 |
|
dvhbase.f |
|- F = ( Scalar ` U ) |
5 |
|
dvhbase.c |
|- C = ( Base ` F ) |
6 |
|
eqid |
|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W ) |
7 |
1 6 3 4
|
dvhsca |
|- ( ( K e. X /\ W e. H ) -> F = ( ( EDRing ` K ) ` W ) ) |
8 |
7
|
fveq2d |
|- ( ( K e. X /\ W e. H ) -> ( Base ` F ) = ( Base ` ( ( EDRing ` K ) ` W ) ) ) |
9 |
5 8
|
syl5eq |
|- ( ( K e. X /\ W e. H ) -> C = ( Base ` ( ( EDRing ` K ) ` W ) ) ) |
10 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
11 |
|
eqid |
|- ( Base ` ( ( EDRing ` K ) ` W ) ) = ( Base ` ( ( EDRing ` K ) ` W ) ) |
12 |
1 10 2 6 11
|
erngbase |
|- ( ( K e. X /\ W e. H ) -> ( Base ` ( ( EDRing ` K ) ` W ) ) = E ) |
13 |
9 12
|
eqtrd |
|- ( ( K e. X /\ W e. H ) -> C = E ) |