Metamath Proof Explorer

Theorem hdmap14lem12

Description: Lemma for proof of part 14 in Baer p. 50. (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 )
hdmap14lem12.o 
|- .0. = ( 0g ` U )
hdmap14lem12.x 
|- ( ph -> X e. ( V \ { .0. } ) )
hdmap14lem12.g 
|- ( ph -> G e. A )
Assertion hdmap14lem12 
|- ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )

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 hdmap14lem12.o 
 |-  .0. = ( 0g ` U )
15 hdmap14lem12.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
16 hdmap14lem12.g 
 |-  ( ph -> G e. A )
17 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
18 10 3ad2ant1 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
19 simp3 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> y e. ( V \ { .0. } ) )
20 19 eldifad 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> y e. V )
21 11 3ad2ant1 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> F e. B )
22 1 2 3 4 5 6 7 8 17 12 13 9 18 20 21 hdmap14lem2a 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> E. g e. A ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) )
23 simp3 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) )
24 eqid 
 |-  ( +g ` U ) = ( +g ` U )
25 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
26 eqid 
 |-  ( +g ` C ) = ( +g ` C )
27 simp11 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ph )
28 27 10 syl 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ( K e. HL /\ W e. H ) )
29 27 15 syl 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> X e. ( V \ { .0. } ) )
30 simp13 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> y e. ( V \ { .0. } ) )
31 27 11 syl 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> F e. B )
32 27 16 syl 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> G e. A )
33 simp2 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> g e. A )
34 simp12 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
35 1 2 3 24 4 14 25 5 6 7 26 8 12 13 9 28 29 30 31 32 33 34 23 hdmap14lem11 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> G = g )
36 35 oveq1d 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ( G .xb ( S ` y ) ) = ( g .xb ( S ` y ) ) )
37 23 36 eqtr4d 
 |-  ( ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) /\ g e. A /\ ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) ) -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) )
38 37 rexlimdv3a 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> ( E. g e. A ( S ` ( F .x. y ) ) = ( g .xb ( S ` y ) ) -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
39 22 38 mpd 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) /\ y e. ( V \ { .0. } ) ) -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) )
40 39 3expia 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) ) -> ( y e. ( V \ { .0. } ) -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
41 40 ralrimiv 
 |-  ( ( ph /\ ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) ) -> A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) )
42 oveq2 
 |-  ( y = X -> ( F .x. y ) = ( F .x. X ) )
43 42 fveq2d 
 |-  ( y = X -> ( S ` ( F .x. y ) ) = ( S ` ( F .x. X ) ) )
44 fveq2 
 |-  ( y = X -> ( S ` y ) = ( S ` X ) )
45 44 oveq2d 
 |-  ( y = X -> ( G .xb ( S ` y ) ) = ( G .xb ( S ` X ) ) )
46 43 45 eqeq12d 
 |-  ( y = X -> ( ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) ) )
47 46 rspcv 
 |-  ( X e. ( V \ { .0. } ) -> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) ) )
48 15 47 syl 
 |-  ( ph -> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) ) )
49 48 imp 
 |-  ( ( ph /\ A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
50 41 49 impbida 
 |-  ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )