Metamath Proof Explorer

Theorem hdmapval2

Description: Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 through hdmaplem4 , which would become obsolete. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapval2.h 
|- H = ( LHyp ` K )
hdmapval2.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapval2.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapval2.v 
|- V = ( Base ` U )
hdmapval2.n 
|- N = ( LSpan ` U )
hdmapval2.c 
|- C = ( ( LCDual ` K ) ` W )
hdmapval2.d 
|- D = ( Base ` C )
hdmapval2.j 
|- J = ( ( HVMap ` K ) ` W )
hdmapval2.i 
|- I = ( ( HDMap1 ` K ) ` W )
hdmapval2.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapval2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapval2.t 
|- ( ph -> T e. V )
hdmapval2.x 
|- ( ph -> X e. V )
hdmapval2.ne 
|- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) )
Assertion hdmapval2 
|- ( ph -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) )

Proof

Step Hyp Ref Expression
1 hdmapval2.h 
 |-  H = ( LHyp ` K )
2 hdmapval2.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapval2.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 hdmapval2.v 
 |-  V = ( Base ` U )
5 hdmapval2.n 
 |-  N = ( LSpan ` U )
6 hdmapval2.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 hdmapval2.d 
 |-  D = ( Base ` C )
8 hdmapval2.j 
 |-  J = ( ( HVMap ` K ) ` W )
9 hdmapval2.i 
 |-  I = ( ( HDMap1 ` K ) ` W )
10 hdmapval2.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmapval2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmapval2.t 
 |-  ( ph -> T e. V )
13 hdmapval2.x 
 |-  ( ph -> X e. V )
14 hdmapval2.ne 
 |-  ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) )
15 eqidd 
 |-  ( ph -> ( S ` T ) = ( S ` T ) )
16 1 3 4 6 7 10 11 12 hdmapcl 
 |-  ( ph -> ( S ` T ) e. D )
17 1 2 3 4 5 6 7 8 9 10 11 12 16 hdmapval2lem 
 |-  ( ph -> ( ( S ` T ) = ( S ` T ) <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
18 15 17 mpbid 
 |-  ( ph -> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) )
19 eleq1 
 |-  ( z = X -> ( z e. ( ( N ` { E } ) u. ( N ` { T } ) ) <-> X e. ( ( N ` { E } ) u. ( N ` { T } ) ) ) )
20 19 notbid 
 |-  ( z = X -> ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) <-> -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) ) )
21 oteq1 
 |-  ( z = X -> <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. = <. X , ( I ` <. E , ( J ` E ) , z >. ) , T >. )
22 oteq3 
 |-  ( z = X -> <. E , ( J ` E ) , z >. = <. E , ( J ` E ) , X >. )
23 22 fveq2d 
 |-  ( z = X -> ( I ` <. E , ( J ` E ) , z >. ) = ( I ` <. E , ( J ` E ) , X >. ) )
24 23 oteq2d 
 |-  ( z = X -> <. X , ( I ` <. E , ( J ` E ) , z >. ) , T >. = <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. )
25 21 24 eqtrd 
 |-  ( z = X -> <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. = <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. )
26 25 fveq2d 
 |-  ( z = X -> ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) )
27 26 eqeq2d 
 |-  ( z = X -> ( ( S ` T ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) <-> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) ) )
28 20 27 imbi12d 
 |-  ( z = X -> ( ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> ( -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) ) ) )
29 28 rspccv 
 |-  ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) -> ( X e. V -> ( -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) ) ) )
30 18 13 14 29 syl3c 
 |-  ( ph -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) )