Metamath Proof Explorer

Theorem hdmap14lem3

Description: Prior to part 14 in Baer p. 49, line 26. (Contributed by NM, 31-May-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. } ) )
hdmap14lem1.f 
|- ( ph -> F e. ( B \ { Z } ) )
Assertion hdmap14lem3 
|- ( ph -> E! g e. ( A \ { Q } ) ( 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 hdmap14lem1.f 
 |-  ( ph -> F e. ( B \ { Z } ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmap14lem1 
 |-  ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
20 19 eqcomd 
 |-  ( ph -> ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) )
21 eqid 
 |-  ( Base ` C ) = ( Base ` C )
22 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
23 1 9 16 lcdlvec 
 |-  ( ph -> C e. LVec )
24 1 2 16 dvhlmod 
 |-  ( ph -> U e. LMod )
25 18 eldifad 
 |-  ( ph -> F e. B )
26 17 eldifad 
 |-  ( ph -> X e. V )
27 3 6 4 7 lmodvscl 
 |-  ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
28 24 25 26 27 syl3anc 
 |-  ( ph -> ( F .x. X ) e. V )
29 1 2 3 9 21 15 16 28 hdmapcl 
 |-  ( ph -> ( S ` ( F .x. X ) ) e. ( Base ` C ) )
30 1 2 3 5 9 22 21 15 16 17 hdmapnzcl 
 |-  ( ph -> ( S ` X ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) )
31 21 12 13 14 10 22 11 23 29 30 lspsneu 
 |-  ( ph -> ( ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) <-> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
32 20 31 mpbid 
 |-  ( ph -> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )