Metamath Proof Explorer

Theorem hdmap14lem13

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 hdmap14lem13 
|- ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. V ( 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 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 hdmap14lem12 
 |-  ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
18 velsn 
 |-  ( y e. { .0. } <-> y = .0. )
19 1 7 10 lcdlmod 
 |-  ( ph -> C e. LMod )
20 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
21 12 8 13 20 lmodvs0 
 |-  ( ( C e. LMod /\ G e. A ) -> ( G .xb ( 0g ` C ) ) = ( 0g ` C ) )
22 19 16 21 syl2anc 
 |-  ( ph -> ( G .xb ( 0g ` C ) ) = ( 0g ` C ) )
23 1 2 14 7 20 9 10 hdmapval0 
 |-  ( ph -> ( S ` .0. ) = ( 0g ` C ) )
24 23 oveq2d 
 |-  ( ph -> ( G .xb ( S ` .0. ) ) = ( G .xb ( 0g ` C ) ) )
25 1 2 10 dvhlmod 
 |-  ( ph -> U e. LMod )
26 5 4 6 14 lmodvs0 
 |-  ( ( U e. LMod /\ F e. B ) -> ( F .x. .0. ) = .0. )
27 25 11 26 syl2anc 
 |-  ( ph -> ( F .x. .0. ) = .0. )
28 27 fveq2d 
 |-  ( ph -> ( S ` ( F .x. .0. ) ) = ( S ` .0. ) )
29 28 23 eqtrd 
 |-  ( ph -> ( S ` ( F .x. .0. ) ) = ( 0g ` C ) )
30 22 24 29 3eqtr4rd 
 |-  ( ph -> ( S ` ( F .x. .0. ) ) = ( G .xb ( S ` .0. ) ) )
31 oveq2 
 |-  ( y = .0. -> ( F .x. y ) = ( F .x. .0. ) )
32 31 fveq2d 
 |-  ( y = .0. -> ( S ` ( F .x. y ) ) = ( S ` ( F .x. .0. ) ) )
33 fveq2 
 |-  ( y = .0. -> ( S ` y ) = ( S ` .0. ) )
34 33 oveq2d 
 |-  ( y = .0. -> ( G .xb ( S ` y ) ) = ( G .xb ( S ` .0. ) ) )
35 32 34 eqeq12d 
 |-  ( y = .0. -> ( ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> ( S ` ( F .x. .0. ) ) = ( G .xb ( S ` .0. ) ) ) )
36 30 35 syl5ibrcom 
 |-  ( ph -> ( y = .0. -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
37 18 36 biimtrid 
 |-  ( ph -> ( y e. { .0. } -> ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
38 37 ralrimiv 
 |-  ( ph -> A. y e. { .0. } ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) )
39 38 biantrud 
 |-  ( ph -> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) /\ A. y e. { .0. } ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) ) )
40 ralunb 
 |-  ( A. y e. ( ( V \ { .0. } ) u. { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) /\ A. y e. { .0. } ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
41 39 40 bitr4di 
 |-  ( ph -> ( A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> A. y e. ( ( V \ { .0. } ) u. { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
42 3 14 lmod0vcl 
 |-  ( U e. LMod -> .0. e. V )
43 difsnid 
 |-  ( .0. e. V -> ( ( V \ { .0. } ) u. { .0. } ) = V )
44 25 42 43 3syl 
 |-  ( ph -> ( ( V \ { .0. } ) u. { .0. } ) = V )
45 44 raleqdv 
 |-  ( ph -> ( A. y e. ( ( V \ { .0. } ) u. { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) <-> A. y e. V ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
46 17 41 45 3bitrd 
 |-  ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. V ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )