Metamath Proof Explorer

Theorem hgmapvs

Description: Part 15 of Baer p. 50 line 6. Also line 15 in Holland95 p. 14. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hgmapvs.h 
|- H = ( LHyp ` K )
hgmapvs.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapvs.v 
|- V = ( Base ` U )
hgmapvs.t 
|- .x. = ( .s ` U )
hgmapvs.r 
|- R = ( Scalar ` U )
hgmapvs.b 
|- B = ( Base ` R )
hgmapvs.c 
|- C = ( ( LCDual ` K ) ` W )
hgmapvs.e 
|- .xb = ( .s ` C )
hgmapvs.s 
|- S = ( ( HDMap ` K ) ` W )
hgmapvs.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapvs.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hgmapvs.x 
|- ( ph -> X e. V )
hgmapvs.f 
|- ( ph -> F e. B )
Assertion hgmapvs 
|- ( ph -> ( S ` ( F .x. X ) ) = ( ( G ` F ) .xb ( S ` X ) ) )

Proof

Step Hyp Ref Expression
1 hgmapvs.h 
 |-  H = ( LHyp ` K )
2 hgmapvs.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapvs.v 
 |-  V = ( Base ` U )
4 hgmapvs.t 
 |-  .x. = ( .s ` U )
5 hgmapvs.r 
 |-  R = ( Scalar ` U )
6 hgmapvs.b 
 |-  B = ( Base ` R )
7 hgmapvs.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 hgmapvs.e 
 |-  .xb = ( .s ` C )
9 hgmapvs.s 
 |-  S = ( ( HDMap ` K ) ` W )
10 hgmapvs.g 
 |-  G = ( ( HGMap ` K ) ` W )
11 hgmapvs.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hgmapvs.x 
 |-  ( ph -> X e. V )
13 hgmapvs.f 
 |-  ( ph -> F e. B )
14 1 2 3 4 5 6 7 8 9 10 11 13 hgmapval 
 |-  ( ph -> ( G ` F ) = ( iota_ g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
15 14 eqcomd 
 |-  ( ph -> ( iota_ g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) = ( G ` F ) )
16 1 2 5 6 10 11 13 hgmapcl 
 |-  ( ph -> ( G ` F ) e. B )
17 1 2 3 4 5 6 7 8 9 11 13 hdmap14lem15 
 |-  ( ph -> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )
18 oveq1 
 |-  ( g = ( G ` F ) -> ( g .xb ( S ` x ) ) = ( ( G ` F ) .xb ( S ` x ) ) )
19 18 eqeq2d 
 |-  ( g = ( G ` F ) -> ( ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) <-> ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) ) )
20 19 ralbidv 
 |-  ( g = ( G ` F ) -> ( A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) <-> A. x e. V ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) ) )
21 20 riota2 
 |-  ( ( ( G ` F ) e. B /\ E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) -> ( A. x e. V ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) <-> ( iota_ g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) = ( G ` F ) ) )
22 16 17 21 syl2anc 
 |-  ( ph -> ( A. x e. V ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) <-> ( iota_ g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) = ( G ` F ) ) )
23 15 22 mpbird 
 |-  ( ph -> A. x e. V ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) )
24 oveq2 
 |-  ( x = X -> ( F .x. x ) = ( F .x. X ) )
25 24 fveq2d 
 |-  ( x = X -> ( S ` ( F .x. x ) ) = ( S ` ( F .x. X ) ) )
26 fveq2 
 |-  ( x = X -> ( S ` x ) = ( S ` X ) )
27 26 oveq2d 
 |-  ( x = X -> ( ( G ` F ) .xb ( S ` x ) ) = ( ( G ` F ) .xb ( S ` X ) ) )
28 25 27 eqeq12d 
 |-  ( x = X -> ( ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) <-> ( S ` ( F .x. X ) ) = ( ( G ` F ) .xb ( S ` X ) ) ) )
29 28 rspcva 
 |-  ( ( X e. V /\ A. x e. V ( S ` ( F .x. x ) ) = ( ( G ` F ) .xb ( S ` x ) ) ) -> ( S ` ( F .x. X ) ) = ( ( G ` F ) .xb ( S ` X ) ) )
30 12 23 29 syl2anc 
 |-  ( ph -> ( S ` ( F .x. X ) ) = ( ( G ` F ) .xb ( S ` X ) ) )