Metamath Proof Explorer

Theorem hdmap11

Description: Part of proof of part 12 in Baer p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015)

Ref Expression
Hypotheses hdmap12d.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmap12d.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap12d.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmap12d.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap12d.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmap12d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmap12d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion hdmap11 ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 hdmap12d.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap12d.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap12d.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmap12d.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5 hdmap12d.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 hdmap12d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 hdmap12d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 eqid ⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
9 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
10 eqid ⊢ ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
11 1 2 3 8 9 10 4 5 6 7 hdmapsub ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) )
12 11 eqeq1d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
13 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
14 eqid ⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
15 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 3 8 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
17 15 6 7 16 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
18 1 2 3 13 9 14 4 5 17 hdmapeq0 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ) )
19 1 9 5 lcdlmod ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
20 lmodgrp ⊢ ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp )
21 19 20 syl ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp )
22 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
23 1 2 3 9 22 4 5 6 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
24 1 2 3 9 22 4 5 7 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
25 22 14 10 grpsubeq0 ⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ) )
26 21 23 24 25 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ) )
27 12 18 26 3bitr3rd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ↔ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ) )
28 lmodgrp ⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Grp )
29 15 28 syl ⊢ ( 𝜑 → 𝑈 ∈ Grp )
30 3 13 8 grpsubeq0 ⊢ ( ( 𝑈 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = 𝑌 ) )
31 29 6 7 30 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = 𝑌 ) )
32 27 31 bitrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )