Metamath Proof Explorer

Theorem hgmapval1

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

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

Proof

Step Hyp Ref Expression
1 hgmapval1.h 
 |-  H = ( LHyp ` K )
2 hgmapval1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapval1.r 
 |-  R = ( Scalar ` U )
4 hgmapval1.i 
 |-  .1. = ( 1r ` R )
5 hgmapval1.g 
 |-  G = ( ( HGMap ` K ) ` W )
6 hgmapval1.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 
 |-  ( Scalar ` ( ( LCDual ` K ) ` W ) ) = ( Scalar ` ( ( LCDual ` K ) ` W ) )
12 eqid 
 |-  ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
13 1 2 3 4 10 11 12 6 lcd1 
 |-  ( ph -> ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = .1. )
14 13 oveq1d 
 |-  ( ph -> ( ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( .1. ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
15 14 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( .1. ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
16 1 10 6 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
17 16 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LMod )
18 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
19 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
20 6 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
21 simp2 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> x e. ( Base ` U ) )
22 1 2 7 10 18 19 20 21 hdmapcl 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` x ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
23 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
24 18 11 23 12 lmodvs1 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( ( ( HDMap ` K ) ` W ) ` x ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) ) -> ( ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( ( ( HDMap ` K ) ` W ) ` x ) )
25 17 22 24 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( 1r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( ( ( HDMap ` K ) ` W ) ` x ) )
26 15 25 eqtr3d 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( .1. ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( ( ( HDMap ` K ) ` W ) ` x ) )
27 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
28 27 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> U e. LMod )
29 eqid 
 |-  ( .s ` U ) = ( .s ` U )
30 7 3 29 4 lmodvs1 
 |-  ( ( U e. LMod /\ x e. ( Base ` U ) ) -> ( .1. ( .s ` U ) x ) = x )
31 28 21 30 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( .1. ( .s ` U ) x ) = x )
32 31 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( .1. ( .s ` U ) x ) ) = ( ( ( HDMap ` K ) ` W ) ` x ) )
33 eqid 
 |-  ( Base ` R ) = ( Base ` R )
34 3 lmodring 
 |-  ( U e. LMod -> R e. Ring )
35 33 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
36 27 34 35 3syl 
 |-  ( ph -> .1. e. ( Base ` R ) )
37 36 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> .1. e. ( Base ` R ) )
38 1 2 7 29 3 33 10 23 19 5 20 21 37 hgmapvs 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( .1. ( .s ` U ) x ) ) = ( ( G ` .1. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
39 26 32 38 3eqtr2rd 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( G ` .1. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( .1. ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
40 eqid 
 |-  ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
41 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
42 1 10 6 lcdlvec 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LVec )
43 42 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LVec )
44 1 2 3 33 5 6 36 hgmapcl 
 |-  ( ph -> ( G ` .1. ) e. ( Base ` R ) )
45 1 2 3 33 10 11 40 6 lcdsbase 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` R ) )
46 44 45 eleqtrrd 
 |-  ( ph -> ( G ` .1. ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
47 46 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( G ` .1. ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
48 36 45 eleqtrrd 
 |-  ( ph -> .1. e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
49 48 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> .1. e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
50 simp3 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> x =/= ( 0g ` U ) )
51 1 2 7 8 10 41 19 20 21 hdmapeq0 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` x ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> x = ( 0g ` U ) ) )
52 51 necon3bid 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` x ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> x =/= ( 0g ` U ) ) )
53 50 52 mpbird 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` x ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) )
54 18 23 11 40 41 43 47 49 22 53 lvecvscan2 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( ( ( G ` .1. ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) = ( .1. ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) <-> ( G ` .1. ) = .1. ) )
55 39 54 mpbid 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ x =/= ( 0g ` U ) ) -> ( G ` .1. ) = .1. )
56 55 rexlimdv3a 
 |-  ( ph -> ( E. x e. ( Base ` U ) x =/= ( 0g ` U ) -> ( G ` .1. ) = .1. ) )
57 9 56 mpd 
 |-  ( ph -> ( G ` .1. ) = .1. )