Metamath Proof Explorer

Theorem hgmapval0

Description: Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hgmapval0.h 
|- H = ( LHyp ` K )
hgmapval0.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapval0.r 
|- R = ( Scalar ` U )
hgmapval0.o 
|- .0. = ( 0g ` R )
hgmapval0.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapval0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hgmapval0 
|- ( ph -> ( G ` .0. ) = .0. )

Proof

Step Hyp Ref Expression
1 hgmapval0.h 
 |-  H = ( LHyp ` K )
2 hgmapval0.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapval0.r 
 |-  R = ( Scalar ` U )
4 hgmapval0.o 
 |-  .0. = ( 0g ` R )
5 hgmapval0.g 
 |-  G = ( ( HGMap ` K ) ` W )
6 hgmapval0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 eqid 
 |-  ( Base ` U ) = ( Base ` U )
8 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
9 1 2 7 8 6 dvh1dim 
 |-  ( ph -> E. x e. ( Base ` U ) x =/= ( 0g ` U ) )
10 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
11 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
12 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
13 6 adantr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( K e. HL /\ W e. H ) )
14 simpr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> x e. ( Base ` U ) )
15 1 2 7 8 10 11 12 13 14 hdmapeq0 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> x = ( 0g ` U ) ) )
16 15 biimpd 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) -> x = ( 0g ` U ) ) )
17 16 necon3ad 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( x =/= ( 0g ` U ) -> -. ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) ) )
18 17 3impia 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> -. ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) )
19 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
20 eqid 
 |-  ( .s ` U ) = ( .s ` U )
21 7 3 20 4 8 lmod0vs 
 |-  ( ( U e. LMod /\ x e. ( Base ` U ) ) -> ( .0. ( .s ` U ) x ) = ( 0g ` U ) )
22 19 21 sylan 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( .0. ( .s ` U ) x ) = ( 0g ` U ) )
23 22 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( .0. ( .s ` U ) x ) ) = ( ( ( HDMap ` K ) ` W ) ` ( 0g ` U ) ) )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
26 3 24 4 lmod0cl 
 |-  ( U e. LMod -> .0. e. ( Base ` R ) )
27 19 26 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
28 27 adantr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> .0. e. ( Base ` R ) )
29 1 2 7 20 3 24 10 25 12 5 13 14 28 hgmapvs 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( .0. ( .s ` U ) x ) ) = ( ( G ` .0. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
30 1 2 8 10 11 12 6 hdmapval0 
 |-  ( ph -> ( ( ( HDMap ` K ) ` W ) ` ( 0g ` U ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) )
31 30 adantr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( 0g ` U ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) )
32 23 29 31 3eqtr3d 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( G ` .0. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) )
33 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
34 eqid 
 |-  ( Scalar ` ( ( LCDual ` K ) ` W ) ) = ( Scalar ` ( ( LCDual ` K ) ` W ) )
35 eqid 
 |-  ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
36 eqid 
 |-  ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
37 1 10 6 lcdlvec 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LVec )
38 37 adantr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LVec )
39 1 2 13 dvhlmod 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> U e. LMod )
40 39 26 syl 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> .0. e. ( Base ` R ) )
41 1 2 3 24 10 34 35 5 13 40 hgmapdcl 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( G ` .0. ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
42 1 2 7 10 33 12 13 14 hdmapcl 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` x ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
43 33 25 34 35 36 11 38 41 42 lvecvs0or 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( G ` .0. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) \/ ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) ) ) )
44 32 43 mpbid 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) \/ ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) ) )
45 44 orcomd 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) \/ ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) )
46 45 ord 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( -. ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) -> ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) )
47 46 3adant3 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( -. ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) -> ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) )
48 18 47 mpd 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
49 48 rexlimdv3a 
 |-  ( ph -> ( E. x e. ( Base ` U ) x =/= ( 0g ` U ) -> ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) )
50 9 49 mpd 
 |-  ( ph -> ( G ` .0. ) = ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
51 1 2 3 4 10 34 36 6 lcd0 
 |-  ( ph -> ( 0g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = .0. )
52 50 51 eqtrd 
 |-  ( ph -> ( G ` .0. ) = .0. )