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 ( 𝜑 → ( ( 𝑆𝑋 ) = ( 𝑆𝑌 ) ↔ 𝑋 = 𝑌 ) )