Metamath Proof Explorer

Theorem djhffval

Description: Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

Ref Expression
Hypothesis djhval.h 
|- H = ( LHyp ` K )
Assertion djhffval 
|- ( K e. X -> ( joinH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 djhval.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. X -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )
6 5 fveq1d 
 |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
7 6 fveq2d 
 |-  ( k = K -> ( Base ` ( ( DVecH ` k ) ` w ) ) = ( Base ` ( ( DVecH ` K ) ` w ) ) )
8 7 pweqd 
 |-  ( k = K -> ~P ( Base ` ( ( DVecH ` k ) ` w ) ) = ~P ( Base ` ( ( DVecH ` K ) ` w ) ) )
9 fveq2 
 |-  ( k = K -> ( ocH ` k ) = ( ocH ` K ) )
10 9 fveq1d 
 |-  ( k = K -> ( ( ocH ` k ) ` w ) = ( ( ocH ` K ) ` w ) )
11 10 fveq1d 
 |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` x ) = ( ( ( ocH ` K ) ` w ) ` x ) )
12 10 fveq1d 
 |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` y ) = ( ( ( ocH ` K ) ` w ) ` y ) )
13 11 12 ineq12d 
 |-  ( k = K -> ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) = ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) )
14 10 13 fveq12d 
 |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) = ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) )
15 8 8 14 mpoeq123dv 
 |-  ( k = K -> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) = ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) ) )
16 4 15 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) ) ) )
17 df-djh 
 |-  joinH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) ) )
18 16 17 1 mptfvmpt 
 |-  ( K e. _V -> ( joinH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) ) ) )
19 2 18 syl 
 |-  ( K e. X -> ( joinH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) ) ) )