Metamath Proof Explorer

Theorem hdmap14lem2a

Description: Prior to part 14 in Baer p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 . (Contributed by NM, 31-May-2015)

Ref Expression
Hypotheses hdmap14lem1a.h 
|- H = ( LHyp ` K )
hdmap14lem1a.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap14lem1a.v 
|- V = ( Base ` U )
hdmap14lem1a.t 
|- .x. = ( .s ` U )
hdmap14lem1a.r 
|- R = ( Scalar ` U )
hdmap14lem1a.b 
|- B = ( Base ` R )
hdmap14lem1a.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap14lem2a.e 
|- .xb = ( .s ` C )
hdmap14lem1a.l 
|- L = ( LSpan ` C )
hdmap14lem2a.p 
|- P = ( Scalar ` C )
hdmap14lem2a.a 
|- A = ( Base ` P )
hdmap14lem1a.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap14lem1a.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap14lem3a.x 
|- ( ph -> X e. V )
hdmap14lem1a.f 
|- ( ph -> F e. B )
Assertion hdmap14lem2a 
|- ( ph -> E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem1a.h 
 |-  H = ( LHyp ` K )
2 hdmap14lem1a.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap14lem1a.v 
 |-  V = ( Base ` U )
4 hdmap14lem1a.t 
 |-  .x. = ( .s ` U )
5 hdmap14lem1a.r 
 |-  R = ( Scalar ` U )
6 hdmap14lem1a.b 
 |-  B = ( Base ` R )
7 hdmap14lem1a.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 hdmap14lem2a.e 
 |-  .xb = ( .s ` C )
9 hdmap14lem1a.l 
 |-  L = ( LSpan ` C )
10 hdmap14lem2a.p 
 |-  P = ( Scalar ` C )
11 hdmap14lem2a.a 
 |-  A = ( Base ` P )
12 hdmap14lem1a.s 
 |-  S = ( ( HDMap ` K ) ` W )
13 hdmap14lem1a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
14 hdmap14lem3a.x 
 |-  ( ph -> X e. V )
15 hdmap14lem1a.f 
 |-  ( ph -> F e. B )
16 fvoveq1 
 |-  ( F = ( 0g ` R ) -> ( S ` ( F .x. X ) ) = ( S ` ( ( 0g ` R ) .x. X ) ) )
17 16 eqeq1d 
 |-  ( F = ( 0g ` R ) -> ( ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> ( S ` ( ( 0g ` R ) .x. X ) ) = ( g .xb ( S ` X ) ) ) )
18 17 rexbidv 
 |-  ( F = ( 0g ` R ) -> ( E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E. g e. A ( S ` ( ( 0g ` R ) .x. X ) ) = ( g .xb ( S ` X ) ) ) )
19 difss 
 |-  ( A \ { ( 0g ` P ) } ) C_ A
20 13 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> ( K e. HL /\ W e. H ) )
21 14 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> X e. V )
22 15 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> F e. B )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 simpr 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> F =/= ( 0g ` R ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 20 21 22 23 24 hdmap14lem1a 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
26 25 eqcomd 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) )
27 eqid 
 |-  ( Base ` C ) = ( Base ` C )
28 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
29 1 7 13 lcdlvec 
 |-  ( ph -> C e. LVec )
30 1 2 13 dvhlmod 
 |-  ( ph -> U e. LMod )
31 3 5 4 6 lmodvscl 
 |-  ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
32 30 15 14 31 syl3anc 
 |-  ( ph -> ( F .x. X ) e. V )
33 1 2 3 7 27 12 13 32 hdmapcl 
 |-  ( ph -> ( S ` ( F .x. X ) ) e. ( Base ` C ) )
34 1 2 3 7 27 12 13 14 hdmapcl 
 |-  ( ph -> ( S ` X ) e. ( Base ` C ) )
35 27 10 11 28 8 9 29 33 34 lspsneq 
 |-  ( ph -> ( ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) <-> E. g e. ( A \ { ( 0g ` P ) } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
36 35 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> ( ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) <-> E. g e. ( A \ { ( 0g ` P ) } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
37 26 36 mpbid 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> E. g e. ( A \ { ( 0g ` P ) } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
38 ssrexv 
 |-  ( ( A \ { ( 0g ` P ) } ) C_ A -> ( E. g e. ( A \ { ( 0g ` P ) } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) -> E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
39 19 37 38 mpsyl 
 |-  ( ( ph /\ F =/= ( 0g ` R ) ) -> E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
40 1 7 13 lcdlmod 
 |-  ( ph -> C e. LMod )
41 10 11 28 lmod0cl 
 |-  ( C e. LMod -> ( 0g ` P ) e. A )
42 40 41 syl 
 |-  ( ph -> ( 0g ` P ) e. A )
43 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
44 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
45 1 2 43 7 44 12 13 hdmapval0 
 |-  ( ph -> ( S ` ( 0g ` U ) ) = ( 0g ` C ) )
46 3 5 4 23 43 lmod0vs 
 |-  ( ( U e. LMod /\ X e. V ) -> ( ( 0g ` R ) .x. X ) = ( 0g ` U ) )
47 30 14 46 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) .x. X ) = ( 0g ` U ) )
48 47 fveq2d 
 |-  ( ph -> ( S ` ( ( 0g ` R ) .x. X ) ) = ( S ` ( 0g ` U ) ) )
49 27 10 8 28 44 lmod0vs 
 |-  ( ( C e. LMod /\ ( S ` X ) e. ( Base ` C ) ) -> ( ( 0g ` P ) .xb ( S ` X ) ) = ( 0g ` C ) )
50 40 34 49 syl2anc 
 |-  ( ph -> ( ( 0g ` P ) .xb ( S ` X ) ) = ( 0g ` C ) )
51 45 48 50 3eqtr4d 
 |-  ( ph -> ( S ` ( ( 0g ` R ) .x. X ) ) = ( ( 0g ` P ) .xb ( S ` X ) ) )
52 oveq1 
 |-  ( g = ( 0g ` P ) -> ( g .xb ( S ` X ) ) = ( ( 0g ` P ) .xb ( S ` X ) ) )
53 52 rspceeqv 
 |-  ( ( ( 0g ` P ) e. A /\ ( S ` ( ( 0g ` R ) .x. X ) ) = ( ( 0g ` P ) .xb ( S ` X ) ) ) -> E. g e. A ( S ` ( ( 0g ` R ) .x. X ) ) = ( g .xb ( S ` X ) ) )
54 42 51 53 syl2anc 
 |-  ( ph -> E. g e. A ( S ` ( ( 0g ` R ) .x. X ) ) = ( g .xb ( S ` X ) ) )
55 18 39 54 pm2.61ne 
 |-  ( ph -> E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )