Metamath Proof Explorer

Theorem hdmap14lem14

Description: Part of proof of part 14 in Baer p. 50 line 3. (Contributed by NM, 6-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 hdmap14lem12.h 
 |-  H = ( LHyp ` K )
2 hdmap14lem12.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap14lem12.v 
 |-  V = ( Base ` U )
4 hdmap14lem12.t 
 |-  .x. = ( .s ` U )
5 hdmap14lem12.r 
 |-  R = ( Scalar ` U )
6 hdmap14lem12.b 
 |-  B = ( Base ` R )
7 hdmap14lem12.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 hdmap14lem12.e 
 |-  .xb = ( .s ` C )
9 hdmap14lem12.s 
 |-  S = ( ( HDMap ` K ) ` W )
10 hdmap14lem12.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 hdmap14lem12.f 
 |-  ( ph -> F e. B )
12 hdmap14lem12.p 
 |-  P = ( Scalar ` C )
13 hdmap14lem12.a 
 |-  A = ( Base ` P )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 1 2 3 14 10 dvh1dim 
 |-  ( ph -> E. y e. V y =/= ( 0g ` U ) )
16 10 3ad2ant1 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
17 3simpc 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> ( y e. V /\ y =/= ( 0g ` U ) ) )
18 eldifsn 
 |-  ( y e. ( V \ { ( 0g ` U ) } ) <-> ( y e. V /\ y =/= ( 0g ` U ) ) )
19 17 18 sylibr 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> y e. ( V \ { ( 0g ` U ) } ) )
20 11 3ad2ant1 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> F e. B )
21 1 2 3 4 14 5 6 7 8 12 13 9 16 19 20 hdmap14lem7 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> E! g e. A ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) )
22 simpl1 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> ph )
23 22 10 syl 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> ( K e. HL /\ W e. H ) )
24 22 11 syl 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> F e. B )
25 19 adantr 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> y e. ( V \ { ( 0g ` U ) } ) )
26 simpr 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> g e. A )
27 1 2 3 4 5 6 7 8 9 23 24 12 13 14 25 26 hdmap14lem13 
 |-  ( ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) /\ g e. A ) -> ( ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) <-> A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
28 27 reubidva 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> ( E! g e. A ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) <-> E! g e. A A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
29 21 28 mpbid 
 |-  ( ( ph /\ y e. V /\ y =/= ( 0g ` U ) ) -> E! g e. A A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )
30 29 rexlimdv3a 
 |-  ( ph -> ( E. y e. V y =/= ( 0g ` U ) -> E! g e. A A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
31 15 30 mpd 
 |-  ( ph -> E! g e. A A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )