Metamath Proof Explorer

Theorem hdmapval2lem

Description: Lemma for hdmapval2 . (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.f 
|- ( ph -> F e. D )
Assertion hdmapval2lem 
|- ( ph -> ( ( S ` T ) = F <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , 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.f 
 |-  ( ph -> F e. D )
14 1 2 3 4 5 6 7 8 9 10 11 12 hdmapval 
 |-  ( ph -> ( S ` T ) = ( iota_ h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
15 14 eqeq1d 
 |-  ( ph -> ( ( S ` T ) = F <-> ( iota_ h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) = F ) )
16 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
17 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
18 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
21 1 19 20 3 4 16 2 11 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
22 1 3 4 16 5 6 17 18 8 11 21 mapdhvmap 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( N ` { E } ) ) = ( ( LSpan ` C ) ` { ( J ` E ) } ) )
23 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
24 1 3 4 16 6 7 23 8 11 21 hvmapcl2 
 |-  ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
25 24 eldifad 
 |-  ( ph -> ( J ` E ) e. D )
26 1 3 4 16 5 6 7 17 18 9 11 22 21 25 12 hdmap1eu 
 |-  ( ph -> E! h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) )
27 nfv 
 |-  F/ h ph
28 nfcvd 
 |-  ( ph -> F/_ h F )
29 nfvd 
 |-  ( ph -> F/ h A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) )
30 eqeq1 
 |-  ( h = F -> ( h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) <-> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) )
31 30 imbi2d 
 |-  ( h = F -> ( ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
32 31 ralbidv 
 |-  ( h = F -> ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
33 32 adantl 
 |-  ( ( ph /\ h = F ) -> ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
34 27 28 29 13 33 riota2df 
 |-  ( ( ph /\ E! h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) -> ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> ( iota_ h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) = F ) )
35 26 34 mpdan 
 |-  ( ph -> ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) <-> ( iota_ h e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> h = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) = F ) )
36 15 35 bitr4d 
 |-  ( ph -> ( ( S ` T ) = F <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )