Metamath Proof Explorer

Theorem hgmap11

Description: The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses hgmap11.h 
|- H = ( LHyp ` K )
hgmap11.u 
|- U = ( ( DVecH ` K ) ` W )
hgmap11.r 
|- R = ( Scalar ` U )
hgmap11.b 
|- B = ( Base ` R )
hgmap11.g 
|- G = ( ( HGMap ` K ) ` W )
hgmap11.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hgmap11.x 
|- ( ph -> X e. B )
hgmap11.y 
|- ( ph -> Y e. B )
Assertion hgmap11 
|- ( ph -> ( ( G ` X ) = ( G ` Y ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 hgmap11.h 
 |-  H = ( LHyp ` K )
2 hgmap11.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmap11.r 
 |-  R = ( Scalar ` U )
4 hgmap11.b 
 |-  B = ( Base ` R )
5 hgmap11.g 
 |-  G = ( ( HGMap ` K ) ` W )
6 hgmap11.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 hgmap11.x 
 |-  ( ph -> X e. B )
8 hgmap11.y 
 |-  ( ph -> Y e. B )
9 eqid 
 |-  ( Base ` U ) = ( Base ` U )
10 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
11 1 2 9 10 6 dvh1dim 
 |-  ( ph -> E. t e. ( Base ` U ) t =/= ( 0g ` U ) )
12 11 adantr 
 |-  ( ( ph /\ ( G ` X ) = ( G ` Y ) ) -> E. t e. ( Base ` U ) t =/= ( 0g ` U ) )
13 simp1r 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` X ) = ( G ` Y ) )
14 13 oveq1d 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
15 eqid 
 |-  ( .s ` U ) = ( .s ` U )
16 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
17 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
18 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
19 simp1l 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ph )
20 19 6 syl 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
21 simp2 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t e. ( Base ` U ) )
22 19 7 syl 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> X e. B )
23 1 2 9 15 3 4 16 17 18 5 20 21 22 hgmapvs 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
24 19 8 syl 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> Y e. B )
25 1 2 9 15 3 4 16 17 18 5 20 21 24 hgmapvs 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) = ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
26 14 23 25 3eqtr4d 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) = ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) )
27 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
28 19 27 syl 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> U e. LMod )
29 9 3 15 4 lmodvscl 
 |-  ( ( U e. LMod /\ X e. B /\ t e. ( Base ` U ) ) -> ( X ( .s ` U ) t ) e. ( Base ` U ) )
30 28 22 21 29 syl3anc 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( X ( .s ` U ) t ) e. ( Base ` U ) )
31 9 3 15 4 lmodvscl 
 |-  ( ( U e. LMod /\ Y e. B /\ t e. ( Base ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
32 28 24 21 31 syl3anc 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
33 1 2 9 18 20 30 32 hdmap11 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) = ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) <-> ( X ( .s ` U ) t ) = ( Y ( .s ` U ) t ) ) )
34 26 33 mpbid 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( X ( .s ` U ) t ) = ( Y ( .s ` U ) t ) )
35 1 2 6 dvhlvec 
 |-  ( ph -> U e. LVec )
36 19 35 syl 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> U e. LVec )
37 simp3 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t =/= ( 0g ` U ) )
38 9 15 3 4 10 36 22 24 21 37 lvecvscan2 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( X ( .s ` U ) t ) = ( Y ( .s ` U ) t ) <-> X = Y ) )
39 34 38 mpbid 
 |-  ( ( ( ph /\ ( G ` X ) = ( G ` Y ) ) /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> X = Y )
40 39 rexlimdv3a 
 |-  ( ( ph /\ ( G ` X ) = ( G ` Y ) ) -> ( E. t e. ( Base ` U ) t =/= ( 0g ` U ) -> X = Y ) )
41 12 40 mpd 
 |-  ( ( ph /\ ( G ` X ) = ( G ` Y ) ) -> X = Y )
42 41 ex 
 |-  ( ph -> ( ( G ` X ) = ( G ` Y ) -> X = Y ) )
43 fveq2 
 |-  ( X = Y -> ( G ` X ) = ( G ` Y ) )
44 42 43 impbid1 
 |-  ( ph -> ( ( G ` X ) = ( G ` Y ) <-> X = Y ) )