Metamath Proof Explorer

Theorem hdmap14lem6

Description: Case where F is zero. (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmap14lem1.h 
|- H = ( LHyp ` K )
hdmap14lem1.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap14lem1.v 
|- V = ( Base ` U )
hdmap14lem1.t 
|- .x. = ( .s ` U )
hdmap14lem3.o 
|- .0. = ( 0g ` U )
hdmap14lem1.r 
|- R = ( Scalar ` U )
hdmap14lem1.b 
|- B = ( Base ` R )
hdmap14lem1.z 
|- Z = ( 0g ` R )
hdmap14lem1.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap14lem2.e 
|- .xb = ( .s ` C )
hdmap14lem1.l 
|- L = ( LSpan ` C )
hdmap14lem2.p 
|- P = ( Scalar ` C )
hdmap14lem2.a 
|- A = ( Base ` P )
hdmap14lem2.q 
|- Q = ( 0g ` P )
hdmap14lem1.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap14lem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap14lem3.x 
|- ( ph -> X e. ( V \ { .0. } ) )
hdmap14lem6.f 
|- ( ph -> F = Z )
Assertion hdmap14lem6 
|- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem1.h 
 |-  H = ( LHyp ` K )
2 hdmap14lem1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap14lem1.v 
 |-  V = ( Base ` U )
4 hdmap14lem1.t 
 |-  .x. = ( .s ` U )
5 hdmap14lem3.o 
 |-  .0. = ( 0g ` U )
6 hdmap14lem1.r 
 |-  R = ( Scalar ` U )
7 hdmap14lem1.b 
 |-  B = ( Base ` R )
8 hdmap14lem1.z 
 |-  Z = ( 0g ` R )
9 hdmap14lem1.c 
 |-  C = ( ( LCDual ` K ) ` W )
10 hdmap14lem2.e 
 |-  .xb = ( .s ` C )
11 hdmap14lem1.l 
 |-  L = ( LSpan ` C )
12 hdmap14lem2.p 
 |-  P = ( Scalar ` C )
13 hdmap14lem2.a 
 |-  A = ( Base ` P )
14 hdmap14lem2.q 
 |-  Q = ( 0g ` P )
15 hdmap14lem1.s 
 |-  S = ( ( HDMap ` K ) ` W )
16 hdmap14lem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
17 hdmap14lem3.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
18 hdmap14lem6.f 
 |-  ( ph -> F = Z )
19 1 9 16 lcdlmod 
 |-  ( ph -> C e. LMod )
20 12 13 14 lmod0cl 
 |-  ( C e. LMod -> Q e. A )
21 19 20 syl 
 |-  ( ph -> Q e. A )
22 eqid 
 |-  ( Base ` C ) = ( Base ` C )
23 17 eldifad 
 |-  ( ph -> X e. V )
24 1 2 3 9 22 15 16 23 hdmapcl 
 |-  ( ph -> ( S ` X ) e. ( Base ` C ) )
25 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
26 22 12 10 14 25 lmod0vs 
 |-  ( ( C e. LMod /\ ( S ` X ) e. ( Base ` C ) ) -> ( Q .xb ( S ` X ) ) = ( 0g ` C ) )
27 19 24 26 syl2anc 
 |-  ( ph -> ( Q .xb ( S ` X ) ) = ( 0g ` C ) )
28 27 eqcomd 
 |-  ( ph -> ( 0g ` C ) = ( Q .xb ( S ` X ) ) )
29 oveq1 
 |-  ( g = Q -> ( g .xb ( S ` X ) ) = ( Q .xb ( S ` X ) ) )
30 29 rspceeqv 
 |-  ( ( Q e. A /\ ( 0g ` C ) = ( Q .xb ( S ` X ) ) ) -> E. g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) )
31 21 28 30 syl2anc 
 |-  ( ph -> E. g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) )
32 1 2 3 5 9 25 22 15 16 17 hdmapnzcl 
 |-  ( ph -> ( S ` X ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) )
33 eldifsni 
 |-  ( ( S ` X ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) -> ( S ` X ) =/= ( 0g ` C ) )
34 32 33 syl 
 |-  ( ph -> ( S ` X ) =/= ( 0g ` C ) )
35 34 neneqd 
 |-  ( ph -> -. ( S ` X ) = ( 0g ` C ) )
36 35 3ad2ant1 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> -. ( S ` X ) = ( 0g ` C ) )
37 simp3l 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( 0g ` C ) = ( g .xb ( S ` X ) ) )
38 37 eqcomd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( g .xb ( S ` X ) ) = ( 0g ` C ) )
39 1 9 16 lcdlvec 
 |-  ( ph -> C e. LVec )
40 39 3ad2ant1 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> C e. LVec )
41 simp2l 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> g e. A )
42 24 3ad2ant1 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( S ` X ) e. ( Base ` C ) )
43 22 10 12 13 14 25 40 41 42 lvecvs0or 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( ( g .xb ( S ` X ) ) = ( 0g ` C ) <-> ( g = Q \/ ( S ` X ) = ( 0g ` C ) ) ) )
44 38 43 mpbid 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( g = Q \/ ( S ` X ) = ( 0g ` C ) ) )
45 44 orcomd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( ( S ` X ) = ( 0g ` C ) \/ g = Q ) )
46 45 ord 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( -. ( S ` X ) = ( 0g ` C ) -> g = Q ) )
47 36 46 mpd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> g = Q )
48 simp3r 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( 0g ` C ) = ( h .xb ( S ` X ) ) )
49 48 eqcomd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( h .xb ( S ` X ) ) = ( 0g ` C ) )
50 simp2r 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> h e. A )
51 22 10 12 13 14 25 40 50 42 lvecvs0or 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( ( h .xb ( S ` X ) ) = ( 0g ` C ) <-> ( h = Q \/ ( S ` X ) = ( 0g ` C ) ) ) )
52 49 51 mpbid 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( h = Q \/ ( S ` X ) = ( 0g ` C ) ) )
53 52 orcomd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( ( S ` X ) = ( 0g ` C ) \/ h = Q ) )
54 53 ord 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> ( -. ( S ` X ) = ( 0g ` C ) -> h = Q ) )
55 36 54 mpd 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> h = Q )
56 47 55 eqtr4d 
 |-  ( ( ph /\ ( g e. A /\ h e. A ) /\ ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) ) -> g = h )
57 56 3exp 
 |-  ( ph -> ( ( g e. A /\ h e. A ) -> ( ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) -> g = h ) ) )
58 57 ralrimivv 
 |-  ( ph -> A. g e. A A. h e. A ( ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) -> g = h ) )
59 oveq1 
 |-  ( g = h -> ( g .xb ( S ` X ) ) = ( h .xb ( S ` X ) ) )
60 59 eqeq2d 
 |-  ( g = h -> ( ( 0g ` C ) = ( g .xb ( S ` X ) ) <-> ( 0g ` C ) = ( h .xb ( S ` X ) ) ) )
61 60 reu4 
 |-  ( E! g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) <-> ( E. g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ A. g e. A A. h e. A ( ( ( 0g ` C ) = ( g .xb ( S ` X ) ) /\ ( 0g ` C ) = ( h .xb ( S ` X ) ) ) -> g = h ) ) )
62 31 58 61 sylanbrc 
 |-  ( ph -> E! g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) )
63 18 oveq1d 
 |-  ( ph -> ( F .x. X ) = ( Z .x. X ) )
64 1 2 16 dvhlmod 
 |-  ( ph -> U e. LMod )
65 3 6 4 8 5 lmod0vs 
 |-  ( ( U e. LMod /\ X e. V ) -> ( Z .x. X ) = .0. )
66 64 23 65 syl2anc 
 |-  ( ph -> ( Z .x. X ) = .0. )
67 63 66 eqtrd 
 |-  ( ph -> ( F .x. X ) = .0. )
68 67 fveq2d 
 |-  ( ph -> ( S ` ( F .x. X ) ) = ( S ` .0. ) )
69 1 2 5 9 25 15 16 hdmapval0 
 |-  ( ph -> ( S ` .0. ) = ( 0g ` C ) )
70 68 69 eqtrd 
 |-  ( ph -> ( S ` ( F .x. X ) ) = ( 0g ` C ) )
71 70 eqeq1d 
 |-  ( ph -> ( ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> ( 0g ` C ) = ( g .xb ( S ` X ) ) ) )
72 71 reubidv 
 |-  ( ph -> ( E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( 0g ` C ) = ( g .xb ( S ` X ) ) ) )
73 62 72 mpbird 
 |-  ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )