Metamath Proof Explorer

Theorem hlhilset

Description: The final Hilbert space constructed from a Hilbert lattice K and an arbitrary hyperplane W in K . (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilset.h 
|- H = ( LHyp ` K )
hlhilset.l 
|- L = ( ( HLHil ` K ) ` W )
hlhilset.u 
|- U = ( ( DVecH ` K ) ` W )
hlhilset.v 
|- V = ( Base ` U )
hlhilset.p 
|- .+ = ( +g ` U )
hlhilset.e 
|- E = ( ( EDRing ` K ) ` W )
hlhilset.g 
|- G = ( ( HGMap ` K ) ` W )
hlhilset.r 
|- R = ( E sSet <. ( *r ` ndx ) , G >. )
hlhilset.t 
|- .x. = ( .s ` U )
hlhilset.s 
|- S = ( ( HDMap ` K ) ` W )
hlhilset.i 
|- ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )
hlhilset.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hlhilset 
|- ( ph -> L = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )

Proof

Step Hyp Ref Expression
1 hlhilset.h 
 |-  H = ( LHyp ` K )
2 hlhilset.l 
 |-  L = ( ( HLHil ` K ) ` W )
3 hlhilset.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 hlhilset.v 
 |-  V = ( Base ` U )
5 hlhilset.p 
 |-  .+ = ( +g ` U )
6 hlhilset.e 
 |-  E = ( ( EDRing ` K ) ` W )
7 hlhilset.g 
 |-  G = ( ( HGMap ` K ) ` W )
8 hlhilset.r 
 |-  R = ( E sSet <. ( *r ` ndx ) , G >. )
9 hlhilset.t 
 |-  .x. = ( .s ` U )
10 hlhilset.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hlhilset.i 
 |-  ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )
12 hlhilset.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 elex 
 |-  ( K e. HL -> K e. _V )
14 13 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. _V )
15 12 14 syl 
 |-  ( ph -> K e. _V )
16 1 fvexi 
 |-  H e. _V
17 16 mptex 
 |-  ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) e. _V
18 nfcv 
 |-  F/_ k K
19 nfcv 
 |-  F/_ k H
20 nfcsb1v 
 |-  F/_ k [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } )
21 19 20 nfmpt 
 |-  F/_ k ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) )
22 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
23 22 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
24 csbeq1a 
 |-  ( k = K -> [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) = [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) )
25 23 24 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) = ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) )
26 df-hlhil 
 |-  HLHil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) )
27 18 21 25 26 fvmptf 
 |-  ( ( K e. _V /\ ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) e. _V ) -> ( HLHil ` K ) = ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) )
28 15 17 27 sylancl 
 |-  ( ph -> ( HLHil ` K ) = ( w e. H |-> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) )
29 15 adantr 
 |-  ( ( ph /\ w = W ) -> K e. _V )
30 fvexd 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( DVecH ` k ) ` w ) e. _V )
31 fvexd 
 |-  ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) -> ( Base ` u ) e. _V )
32 id 
 |-  ( v = ( Base ` u ) -> v = ( Base ` u ) )
33 id 
 |-  ( u = ( ( DVecH ` k ) ` w ) -> u = ( ( DVecH ` k ) ` w ) )
34 simpr 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> k = K )
35 34 fveq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( DVecH ` k ) = ( DVecH ` K ) )
36 simplr 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> w = W )
37 35 36 fveq12d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` W ) )
38 37 3 eqtr4di 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( DVecH ` k ) ` w ) = U )
39 33 38 sylan9eqr 
 |-  ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) -> u = U )
40 39 fveq2d 
 |-  ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) -> ( Base ` u ) = ( Base ` U ) )
41 40 4 eqtr4di 
 |-  ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) -> ( Base ` u ) = V )
42 32 41 sylan9eqr 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> v = V )
43 42 opeq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , V >. )
44 39 adantr 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> u = U )
45 44 fveq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( +g ` u ) = ( +g ` U ) )
46 45 5 eqtr4di 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( +g ` u ) = .+ )
47 46 opeq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> <. ( +g ` ndx ) , ( +g ` u ) >. = <. ( +g ` ndx ) , .+ >. )
48 34 fveq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( EDRing ` k ) = ( EDRing ` K ) )
49 48 36 fveq12d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( EDRing ` k ) ` w ) = ( ( EDRing ` K ) ` W ) )
50 49 6 eqtr4di 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( EDRing ` k ) ` w ) = E )
51 34 fveq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( HGMap ` k ) = ( HGMap ` K ) )
52 51 36 fveq12d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( HGMap ` k ) ` w ) = ( ( HGMap ` K ) ` W ) )
53 52 7 eqtr4di 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( HGMap ` k ) ` w ) = G )
54 53 opeq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. = <. ( *r ` ndx ) , G >. )
55 50 54 oveq12d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) = ( E sSet <. ( *r ` ndx ) , G >. ) )
56 55 8 eqtr4di 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) = R )
57 56 opeq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. = <. ( Scalar ` ndx ) , R >. )
58 57 ad2antrr 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. = <. ( Scalar ` ndx ) , R >. )
59 43 47 58 tpeq123d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } = { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } )
60 44 fveq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( .s ` u ) = ( .s ` U ) )
61 60 9 eqtr4di 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( .s ` u ) = .x. )
62 61 opeq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> <. ( .s ` ndx ) , ( .s ` u ) >. = <. ( .s ` ndx ) , .x. >. )
63 34 fveq2d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( HDMap ` k ) = ( HDMap ` K ) )
64 63 36 fveq12d 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( HDMap ` k ) ` w ) = ( ( HDMap ` K ) ` W ) )
65 64 10 eqtr4di 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> ( ( HDMap ` k ) ` w ) = S )
66 65 ad2antrr 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( ( HDMap ` k ) ` w ) = S )
67 66 fveq1d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( ( ( HDMap ` k ) ` w ) ` y ) = ( S ` y ) )
68 67 fveq1d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) = ( ( S ` y ) ` x ) )
69 42 42 68 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) )
70 69 11 eqtr4di 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) = ., )
71 70 opeq2d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. = <. ( .i ` ndx ) , ., >. )
72 62 71 preq12d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } = { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )
73 59 72 uneq12d 
 |-  ( ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) /\ v = ( Base ` u ) ) -> ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
74 31 73 csbied 
 |-  ( ( ( ( ph /\ w = W ) /\ k = K ) /\ u = ( ( DVecH ` k ) ` w ) ) -> [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
75 30 74 csbied 
 |-  ( ( ( ph /\ w = W ) /\ k = K ) -> [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
76 29 75 csbied 
 |-  ( ( ph /\ w = W ) -> [_ K / k ]_ [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
77 12 simprd 
 |-  ( ph -> W e. H )
78 tpex 
 |-  { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } e. _V
79 prex 
 |-  { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V
80 78 79 unex 
 |-  ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V
81 80 a1i 
 |-  ( ph -> ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V )
82 28 76 77 81 fvmptd 
 |-  ( ph -> ( ( HLHil ` K ) ` W ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
83 2 82 syl5eq 
 |-  ( ph -> L = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )