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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hgmap11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmap11.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hgmap11.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hgmap11.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmap11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hgmap11.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
hgmap11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion hgmap11 ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 hgmap11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmap11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmap11.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4 hgmap11.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
5 hgmap11.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
6 hgmap11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 hgmap11.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 hgmap11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
10 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
11 1 2 9 10 6 dvh1dim ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( Base ‘ 𝑈 ) 𝑡 ≠ ( 0g ‘ 𝑈 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) → ∃ 𝑡 ∈ ( Base ‘ 𝑈 ) 𝑡 ≠ ( 0g ‘ 𝑈 ) )
13 simp1r ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) )
14 13 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
16 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
18 eqid ⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
19 simp1l ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝜑 )
20 19 6 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑡 ∈ ( Base ‘ 𝑈 ) )
22 19 7 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
23 1 2 9 15 3 4 16 17 18 5 20 21 22 hgmapvs ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
24 19 8 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑌 ∈ 𝐵 )
25 1 2 9 15 3 4 16 17 18 5 20 21 24 hgmapvs ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
26 14 23 25 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) )
27 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
28 19 27 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
29 9 3 15 4 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
30 28 22 21 29 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
31 9 3 15 4 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝐵 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
32 28 24 21 31 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
33 1 2 9 18 20 30 32 hdmap11 ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) ↔ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) = ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) )
34 26 33 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) = ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) )
35 1 2 6 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
36 19 35 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LVec )
37 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑡 ≠ ( 0g ‘ 𝑈 ) )
38 9 15 3 4 10 36 22 24 21 37 lvecvscan2 ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) = ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ↔ 𝑋 = 𝑌 ) )
39 34 38 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 = 𝑌 )
40 39 rexlimdv3a ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) → ( ∃ 𝑡 ∈ ( Base ‘ 𝑈 ) 𝑡 ≠ ( 0g ‘ 𝑈 ) → 𝑋 = 𝑌 ) )
41 12 40 mpd ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) → 𝑋 = 𝑌 )
42 41 ex ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
43 fveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) )
44 42 43 impbid1 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )