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 
|- H = ( LHyp ` K )
hdmap12d.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap12d.v 
|- V = ( Base ` U )
hdmap12d.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap12d.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap12d.x 
|- ( ph -> X e. V )
hdmap12d.y 
|- ( ph -> Y e. V )
Assertion hdmap11 
|- ( ph -> ( ( S ` X ) = ( S ` Y ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 hdmap12d.h 
 |-  H = ( LHyp ` K )
2 hdmap12d.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap12d.v 
 |-  V = ( Base ` U )
4 hdmap12d.s 
 |-  S = ( ( HDMap ` K ) ` W )
5 hdmap12d.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 hdmap12d.x 
 |-  ( ph -> X e. V )
7 hdmap12d.y 
 |-  ( ph -> Y e. V )
8 eqid 
 |-  ( -g ` U ) = ( -g ` U )
9 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
10 eqid 
 |-  ( -g ` ( ( LCDual ` K ) ` W ) ) = ( -g ` ( ( LCDual ` K ) ` W ) )
11 1 2 3 8 9 10 4 5 6 7 hdmapsub 
 |-  ( ph -> ( S ` ( X ( -g ` U ) Y ) ) = ( ( S ` X ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) )
12 11 eqeq1d 
 |-  ( ph -> ( ( S ` ( X ( -g ` U ) Y ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( ( S ` X ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) ) )
13 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
14 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
15 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
16 3 8 lmodvsubcl 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X ( -g ` U ) Y ) e. V )
17 15 6 7 16 syl3anc 
 |-  ( ph -> ( X ( -g ` U ) Y ) e. V )
18 1 2 3 13 9 14 4 5 17 hdmapeq0 
 |-  ( ph -> ( ( S ` ( X ( -g ` U ) Y ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( X ( -g ` U ) Y ) = ( 0g ` U ) ) )
19 1 9 5 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
20 lmodgrp 
 |-  ( ( ( LCDual ` K ) ` W ) e. LMod -> ( ( LCDual ` K ) ` W ) e. Grp )
21 19 20 syl 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. Grp )
22 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
23 1 2 3 9 22 4 5 6 hdmapcl 
 |-  ( ph -> ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
24 1 2 3 9 22 4 5 7 hdmapcl 
 |-  ( ph -> ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
25 22 14 10 grpsubeq0 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. Grp /\ ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) /\ ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) ) -> ( ( ( S ` X ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( S ` X ) = ( S ` Y ) ) )
26 21 23 24 25 syl3anc 
 |-  ( ph -> ( ( ( S ` X ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( S ` X ) = ( S ` Y ) ) )
27 12 18 26 3bitr3rd 
 |-  ( ph -> ( ( S ` X ) = ( S ` Y ) <-> ( X ( -g ` U ) Y ) = ( 0g ` U ) ) )
28 lmodgrp 
 |-  ( U e. LMod -> U e. Grp )
29 15 28 syl 
 |-  ( ph -> U e. Grp )
30 3 13 8 grpsubeq0 
 |-  ( ( U e. Grp /\ X e. V /\ Y e. V ) -> ( ( X ( -g ` U ) Y ) = ( 0g ` U ) <-> X = Y ) )
31 29 6 7 30 syl3anc 
 |-  ( ph -> ( ( X ( -g ` U ) Y ) = ( 0g ` U ) <-> X = Y ) )
32 27 31 bitrd 
 |-  ( ph -> ( ( S ` X ) = ( S ` Y ) <-> X = Y ) )