Metamath Proof Explorer

Theorem djavalN

Description: Subspace join for DVecA partial vector space. (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 djavalN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ._|_ ` ( ( ._|_ ` 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 2 3 4 5 djafvalN 
 |-  ( ( K e. HL /\ W e. H ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
7 6 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
8 7 oveqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( X ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) Y ) )
9 2 fvexi 
 |-  T e. _V
10 9 elpw2 
 |-  ( X e. ~P T <-> X C_ T )
11 10 biimpri 
 |-  ( X C_ T -> X e. ~P T )
12 11 ad2antrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> X e. ~P T )
13 9 elpw2 
 |-  ( Y e. ~P T <-> Y C_ T )
14 13 biimpri 
 |-  ( Y C_ T -> Y e. ~P T )
15 14 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> Y e. ~P T )
16 fvexd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) e. _V )
17 fveq2 
 |-  ( x = X -> ( ._|_ ` x ) = ( ._|_ ` X ) )
18 17 ineq1d 
 |-  ( x = X -> ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` y ) ) )
19 18 fveq2d 
 |-  ( x = X -> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` y ) ) ) )
20 fveq2 
 |-  ( y = Y -> ( ._|_ ` y ) = ( ._|_ ` Y ) )
21 20 ineq2d 
 |-  ( y = Y -> ( ( ._|_ ` X ) i^i ( ._|_ ` y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
22 21 fveq2d 
 |-  ( y = Y -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` y ) ) ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
23 eqid 
 |-  ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) )
24 19 22 23 ovmpog 
 |-  ( ( X e. ~P T /\ Y e. ~P T /\ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) e. _V ) -> ( X ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
25 12 15 16 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
26 8 25 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )