Metamath Proof Explorer

Theorem hdmapip0

Description: Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015)

Ref Expression
Hypotheses hdmapip0.h 
|- H = ( LHyp ` K )
hdmapip0.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapip0.v 
|- V = ( Base ` U )
hdmapip0.o 
|- .0. = ( 0g ` U )
hdmapip0.r 
|- R = ( Scalar ` U )
hdmapip0.z 
|- Z = ( 0g ` R )
hdmapip0.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapip0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapip0.x 
|- ( ph -> X e. V )
Assertion hdmapip0 
|- ( ph -> ( ( ( S ` X ) ` X ) = Z <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 hdmapip0.h 
 |-  H = ( LHyp ` K )
2 hdmapip0.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapip0.v 
 |-  V = ( Base ` U )
4 hdmapip0.o 
 |-  .0. = ( 0g ` U )
5 hdmapip0.r 
 |-  R = ( Scalar ` U )
6 hdmapip0.z 
 |-  Z = ( 0g ` R )
7 hdmapip0.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmapip0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmapip0.x 
 |-  ( ph -> X e. V )
10 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11 8 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> ( K e. HL /\ W e. H ) )
12 9 anim1i 
 |-  ( ( ph /\ X =/= .0. ) -> ( X e. V /\ X =/= .0. ) )
13 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
14 12 13 sylibr 
 |-  ( ( ph /\ X =/= .0. ) -> X e. ( V \ { .0. } ) )
15 1 10 2 3 4 11 14 dochnel 
 |-  ( ( ph /\ X =/= .0. ) -> -. X e. ( ( ( ocH ` K ) ` W ) ` { X } ) )
16 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
17 eqid 
 |-  ( LKer ` U ) = ( LKer ` U )
18 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
19 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
20 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
21 1 2 3 19 20 7 8 9 hdmapcl 
 |-  ( ph -> ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
22 1 19 20 2 16 8 21 lcdvbaselfl 
 |-  ( ph -> ( S ` X ) e. ( LFnl ` U ) )
23 3 5 6 16 17 18 22 9 ellkr2 
 |-  ( ph -> ( X e. ( ( LKer ` U ) ` ( S ` X ) ) <-> ( ( S ` X ) ` X ) = Z ) )
24 23 biimpar 
 |-  ( ( ph /\ ( ( S ` X ) ` X ) = Z ) -> X e. ( ( LKer ` U ) ` ( S ` X ) ) )
25 1 10 2 3 16 17 7 8 9 hdmaplkr 
 |-  ( ph -> ( ( LKer ` U ) ` ( S ` X ) ) = ( ( ( ocH ` K ) ` W ) ` { X } ) )
26 25 adantr 
 |-  ( ( ph /\ ( ( S ` X ) ` X ) = Z ) -> ( ( LKer ` U ) ` ( S ` X ) ) = ( ( ( ocH ` K ) ` W ) ` { X } ) )
27 24 26 eleqtrd 
 |-  ( ( ph /\ ( ( S ` X ) ` X ) = Z ) -> X e. ( ( ( ocH ` K ) ` W ) ` { X } ) )
28 27 ex 
 |-  ( ph -> ( ( ( S ` X ) ` X ) = Z -> X e. ( ( ( ocH ` K ) ` W ) ` { X } ) ) )
29 28 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( ( S ` X ) ` X ) = Z -> X e. ( ( ( ocH ` K ) ` W ) ` { X } ) ) )
30 15 29 mtod 
 |-  ( ( ph /\ X =/= .0. ) -> -. ( ( S ` X ) ` X ) = Z )
31 30 neqned 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( S ` X ) ` X ) =/= Z )
32 31 ex 
 |-  ( ph -> ( X =/= .0. -> ( ( S ` X ) ` X ) =/= Z ) )
33 32 necon4d 
 |-  ( ph -> ( ( ( S ` X ) ` X ) = Z -> X = .0. ) )
34 33 imp 
 |-  ( ( ph /\ ( ( S ` X ) ` X ) = Z ) -> X = .0. )
35 fveq2 
 |-  ( X = .0. -> ( ( S ` X ) ` X ) = ( ( S ` X ) ` .0. ) )
36 5 6 4 16 lfl0 
 |-  ( ( U e. LMod /\ ( S ` X ) e. ( LFnl ` U ) ) -> ( ( S ` X ) ` .0. ) = Z )
37 18 22 36 syl2anc 
 |-  ( ph -> ( ( S ` X ) ` .0. ) = Z )
38 35 37 sylan9eqr 
 |-  ( ( ph /\ X = .0. ) -> ( ( S ` X ) ` X ) = Z )
39 34 38 impbida 
 |-  ( ph -> ( ( ( S ` X ) ` X ) = Z <-> X = .0. ) )