Metamath Proof Explorer

Theorem djafvalN

Description: Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djaval.h 
|- H = ( LHyp ` K )
djaval.t 
|- T = ( ( LTrn ` K ) ` W )
djaval.i 
|- I = ( ( DIsoA ` K ) ` W )
djaval.n 
|- ._|_ = ( ( ocA ` K ) ` W )
djaval.j 
|- J = ( ( vA ` K ) ` W )
Assertion djafvalN 
|- ( ( K e. V /\ W e. H ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 djaval.h 
 |-  H = ( LHyp ` K )
2 djaval.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 djaval.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 djaval.n 
 |-  ._|_ = ( ( ocA ` K ) ` W )
5 djaval.j 
 |-  J = ( ( vA ` K ) ` W )
6 1 djaffvalN 
 |-  ( K e. V -> ( vA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) )
7 6 fveq1d 
 |-  ( K e. V -> ( ( vA ` K ) ` W ) = ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) ` W ) )
8 5 7 eqtrid 
 |-  ( K e. V -> J = ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) ` W ) )
9 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
10 9 2 eqtr4di 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = T )
11 10 pweqd 
 |-  ( w = W -> ~P ( ( LTrn ` K ) ` w ) = ~P T )
12 fveq2 
 |-  ( w = W -> ( ( ocA ` K ) ` w ) = ( ( ocA ` K ) ` W ) )
13 12 4 eqtr4di 
 |-  ( w = W -> ( ( ocA ` K ) ` w ) = ._|_ )
14 13 fveq1d 
 |-  ( w = W -> ( ( ( ocA ` K ) ` w ) ` x ) = ( ._|_ ` x ) )
15 13 fveq1d 
 |-  ( w = W -> ( ( ( ocA ` K ) ` w ) ` y ) = ( ._|_ ` y ) )
16 14 15 ineq12d 
 |-  ( w = W -> ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) = ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) )
17 13 16 fveq12d 
 |-  ( w = W -> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) = ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) )
18 11 11 17 mpoeq123dv 
 |-  ( w = W -> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
19 eqid 
 |-  ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) )
20 2 fvexi 
 |-  T e. _V
21 20 pwex 
 |-  ~P T e. _V
22 21 21 mpoex 
 |-  ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) e. _V
23 18 19 22 fvmpt 
 |-  ( W e. H -> ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) ` W ) = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
24 8 23 sylan9eq 
 |-  ( ( K e. V /\ W e. H ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )