Step |
Hyp |
Ref |
Expression |
1 |
|
hlhilnvl.h |
|- H = ( LHyp ` K ) |
2 |
|
hlhilnvl.u |
|- U = ( ( HLHil ` K ) ` W ) |
3 |
|
hlhilnvl.r |
|- R = ( Scalar ` U ) |
4 |
|
hlhilnvl.i |
|- .* = ( ( HGMap ` K ) ` W ) |
5 |
|
hlhilnvl.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
6 |
|
fvex |
|- ( ( EDRing ` K ) ` W ) e. _V |
7 |
4
|
fvexi |
|- .* e. _V |
8 |
|
starvid |
|- *r = Slot ( *r ` ndx ) |
9 |
8
|
setsid |
|- ( ( ( ( EDRing ` K ) ` W ) e. _V /\ .* e. _V ) -> .* = ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) ) ) |
10 |
6 7 9
|
mp2an |
|- .* = ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) ) |
11 |
|
eqid |
|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W ) |
12 |
|
eqid |
|- ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) |
13 |
1 2 5 11 4 12
|
hlhilsca |
|- ( ph -> ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = ( Scalar ` U ) ) |
14 |
13 3
|
eqtr4di |
|- ( ph -> ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = R ) |
15 |
14
|
fveq2d |
|- ( ph -> ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) ) = ( *r ` R ) ) |
16 |
10 15
|
syl5eq |
|- ( ph -> .* = ( *r ` R ) ) |