Metamath Proof Explorer

Theorem djhfval

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

Ref Expression
Hypotheses djhval.h 
|- H = ( LHyp ` K )
djhval.u 
|- U = ( ( DVecH ` K ) ` W )
djhval.v 
|- V = ( Base ` U )
djhval.o 
|- ._|_ = ( ( ocH ` K ) ` W )
djhval.j 
|- .\/ = ( ( joinH ` K ) ` W )
Assertion djhfval 
|- ( ( K e. X /\ W e. H ) -> .\/ = ( x e. ~P V , y e. ~P V |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 djhval.h 
 |-  H = ( LHyp ` K )
2 djhval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 djhval.v 
 |-  V = ( Base ` U )
4 djhval.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
5 djhval.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
6 1 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 ) ) ) ) ) )
7 6 fveq1d 
 |-  ( K e. X -> ( ( joinH ` K ) ` W ) = ( ( 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 ) ) ) ) ) ` W ) )
8 5 7 syl5eq 
 |-  ( K e. X -> .\/ = ( ( 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 ) ) ) ) ) ` W ) )
9 2fveq3 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = ( Base ` ( ( DVecH ` K ) ` W ) ) )
10 2 fveq2i 
 |-  ( Base ` U ) = ( Base ` ( ( DVecH ` K ) ` W ) )
11 3 10 eqtri 
 |-  V = ( Base ` ( ( DVecH ` K ) ` W ) )
12 9 11 eqtr4di 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = V )
13 12 pweqd 
 |-  ( w = W -> ~P ( Base ` ( ( DVecH ` K ) ` w ) ) = ~P V )
14 fveq2 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ( ( ocH ` K ) ` W ) )
15 14 4 eqtr4di 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ._|_ )
16 15 fveq1d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` x ) = ( ._|_ ` x ) )
17 15 fveq1d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` y ) = ( ._|_ ` y ) )
18 16 17 ineq12d 
 |-  ( w = W -> ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) = ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) )
19 15 18 fveq12d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` ( ( ( ( ocH ` K ) ` w ) ` x ) i^i ( ( ( ocH ` K ) ` w ) ` y ) ) ) = ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) )
20 13 13 19 mpoeq123dv 
 |-  ( w = W -> ( 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 V , y e. ~P V |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
21 eqid 
 |-  ( 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 ) ) ) ) ) = ( 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 ) ) ) ) )
22 3 fvexi 
 |-  V e. _V
23 22 pwex 
 |-  ~P V e. _V
24 23 23 mpoex 
 |-  ( x e. ~P V , y e. ~P V |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) e. _V
25 20 21 24 fvmpt 
 |-  ( W e. H -> ( ( 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 ) ) ) ) ) ` W ) = ( x e. ~P V , y e. ~P V |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
26 8 25 sylan9eq 
 |-  ( ( K e. X /\ W e. H ) -> .\/ = ( x e. ~P V , y e. ~P V |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )