# 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}=\mathrm{LHyp}\left({K}\right)$
hgmap11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hgmap11.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hgmap11.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hgmap11.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hgmap11.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hgmap11.x ${⊢}{\phi }\to {X}\in {B}$
hgmap11.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion hgmap11 ${⊢}{\phi }\to \left({G}\left({X}\right)={G}\left({Y}\right)↔{X}={Y}\right)$

### Proof

Step Hyp Ref Expression
1 hgmap11.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hgmap11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hgmap11.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
4 hgmap11.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
5 hgmap11.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
6 hgmap11.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 hgmap11.x ${⊢}{\phi }\to {X}\in {B}$
8 hgmap11.y ${⊢}{\phi }\to {Y}\in {B}$
9 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
10 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
11 1 2 9 10 6 dvh1dim ${⊢}{\phi }\to \exists {t}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}{t}\ne {0}_{{U}}$
12 11 adantr ${⊢}\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\to \exists {t}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}{t}\ne {0}_{{U}}$
13 simp1r ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {G}\left({X}\right)={G}\left({Y}\right)$
14 13 oveq1d ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {G}\left({X}\right){\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({t}\right)={G}\left({Y}\right){\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({t}\right)$
15 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
16 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
17 eqid ${⊢}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
18 eqid ${⊢}\mathrm{HDMap}\left({K}\right)\left({W}\right)=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
19 simp1l ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {\phi }$
20 19 6 syl ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
21 simp2 ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {t}\in {\mathrm{Base}}_{{U}}$
22 19 7 syl ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {X}\in {B}$
23 1 2 9 15 3 4 16 17 18 5 20 21 22 hgmapvs ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({X}{\cdot }_{{U}}{t}\right)={G}\left({X}\right){\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({t}\right)$
24 19 8 syl ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {Y}\in {B}$
25 1 2 9 15 3 4 16 17 18 5 20 21 24 hgmapvs ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({Y}{\cdot }_{{U}}{t}\right)={G}\left({Y}\right){\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({t}\right)$
26 14 23 25 3eqtr4d ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({X}{\cdot }_{{U}}{t}\right)=\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({Y}{\cdot }_{{U}}{t}\right)$
27 1 2 6 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
28 19 27 syl ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {U}\in \mathrm{LMod}$
29 9 3 15 4 lmodvscl ${⊢}\left({U}\in \mathrm{LMod}\wedge {X}\in {B}\wedge {t}\in {\mathrm{Base}}_{{U}}\right)\to {X}{\cdot }_{{U}}{t}\in {\mathrm{Base}}_{{U}}$
30 28 22 21 29 syl3anc ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {X}{\cdot }_{{U}}{t}\in {\mathrm{Base}}_{{U}}$
31 9 3 15 4 lmodvscl ${⊢}\left({U}\in \mathrm{LMod}\wedge {Y}\in {B}\wedge {t}\in {\mathrm{Base}}_{{U}}\right)\to {Y}{\cdot }_{{U}}{t}\in {\mathrm{Base}}_{{U}}$
32 28 24 21 31 syl3anc ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {Y}{\cdot }_{{U}}{t}\in {\mathrm{Base}}_{{U}}$
33 1 2 9 18 20 30 32 hdmap11 ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \left(\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({X}{\cdot }_{{U}}{t}\right)=\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({Y}{\cdot }_{{U}}{t}\right)↔{X}{\cdot }_{{U}}{t}={Y}{\cdot }_{{U}}{t}\right)$
34 26 33 mpbid ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {X}{\cdot }_{{U}}{t}={Y}{\cdot }_{{U}}{t}$
35 1 2 6 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
36 19 35 syl ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {U}\in \mathrm{LVec}$
37 simp3 ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {t}\ne {0}_{{U}}$
38 9 15 3 4 10 36 22 24 21 37 lvecvscan2 ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to \left({X}{\cdot }_{{U}}{t}={Y}{\cdot }_{{U}}{t}↔{X}={Y}\right)$
39 34 38 mpbid ${⊢}\left(\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\wedge {t}\in {\mathrm{Base}}_{{U}}\wedge {t}\ne {0}_{{U}}\right)\to {X}={Y}$
40 39 rexlimdv3a ${⊢}\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\to \left(\exists {t}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}{t}\ne {0}_{{U}}\to {X}={Y}\right)$
41 12 40 mpd ${⊢}\left({\phi }\wedge {G}\left({X}\right)={G}\left({Y}\right)\right)\to {X}={Y}$
42 41 ex ${⊢}{\phi }\to \left({G}\left({X}\right)={G}\left({Y}\right)\to {X}={Y}\right)$
43 fveq2 ${⊢}{X}={Y}\to {G}\left({X}\right)={G}\left({Y}\right)$
44 42 43 impbid1 ${⊢}{\phi }\to \left({G}\left({X}\right)={G}\left({Y}\right)↔{X}={Y}\right)$