Metamath Proof Explorer

Theorem hgmapfval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

Ref Expression
Hypotheses hgmapval.h 
|- H = ( LHyp ` K )
hgmapfval.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapfval.v 
|- V = ( Base ` U )
hgmapfval.t 
|- .x. = ( .s ` U )
hgmapfval.r 
|- R = ( Scalar ` U )
hgmapfval.b 
|- B = ( Base ` R )
hgmapfval.c 
|- C = ( ( LCDual ` K ) ` W )
hgmapfval.s 
|- .xb = ( .s ` C )
hgmapfval.m 
|- M = ( ( HDMap ` K ) ` W )
hgmapfval.i 
|- I = ( ( HGMap ` K ) ` W )
hgmapfval.k 
|- ( ph -> ( K e. Y /\ W e. H ) )
Assertion hgmapfval 
|- ( ph -> I = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgmapval.h 
 |-  H = ( LHyp ` K )
2 hgmapfval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapfval.v 
 |-  V = ( Base ` U )
4 hgmapfval.t 
 |-  .x. = ( .s ` U )
5 hgmapfval.r 
 |-  R = ( Scalar ` U )
6 hgmapfval.b 
 |-  B = ( Base ` R )
7 hgmapfval.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 hgmapfval.s 
 |-  .xb = ( .s ` C )
9 hgmapfval.m 
 |-  M = ( ( HDMap ` K ) ` W )
10 hgmapfval.i 
 |-  I = ( ( HGMap ` K ) ` W )
11 hgmapfval.k 
 |-  ( ph -> ( K e. Y /\ W e. H ) )
12 1 hgmapffval 
 |-  ( K e. Y -> ( HGMap ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )
13 12 fveq1d 
 |-  ( K e. Y -> ( ( HGMap ` K ) ` W ) = ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) ` W ) )
14 10 13 syl5eq 
 |-  ( K e. Y -> I = ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) ` W ) )
15 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
16 15 2 eqtr4di 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = U )
17 fveq2 
 |-  ( w = W -> ( ( HDMap ` K ) ` w ) = ( ( HDMap ` K ) ` W ) )
18 17 9 eqtr4di 
 |-  ( w = W -> ( ( HDMap ` K ) ` w ) = M )
19 2fveq3 
 |-  ( w = W -> ( .s ` ( ( LCDual ` K ) ` w ) ) = ( .s ` ( ( LCDual ` K ) ` W ) ) )
20 19 oveqd 
 |-  ( w = W -> ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) )
21 20 eqeq2d 
 |-  ( w = W -> ( ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) <-> ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) )
22 21 ralbidv 
 |-  ( w = W -> ( A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) <-> A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) )
23 22 riotabidv 
 |-  ( w = W -> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) = ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) )
24 23 mpteq2dv 
 |-  ( w = W -> ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) = ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) )
25 24 eleq2d 
 |-  ( w = W -> ( a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) <-> a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) ) )
26 18 25 sbceqbid 
 |-  ( w = W -> ( [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) <-> [. M / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) ) )
27 26 sbcbidv 
 |-  ( w = W -> ( [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) <-> [. ( Base ` ( Scalar ` u ) ) / b ]. [. M / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) ) )
28 16 27 sbceqbid 
 |-  ( w = W -> ( [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) <-> [. U / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. M / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) ) )
29 2 fvexi 
 |-  U e. _V
30 fvex 
 |-  ( Base ` ( Scalar ` u ) ) e. _V
31 9 fvexi 
 |-  M e. _V
32 simp2 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> b = ( Base ` ( Scalar ` u ) ) )
33 simp1 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> u = U )
34 33 fveq2d 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> ( Scalar ` u ) = ( Scalar ` U ) )
35 34 5 eqtr4di 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> ( Scalar ` u ) = R )
36 35 fveq2d 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> ( Base ` ( Scalar ` u ) ) = ( Base ` R ) )
37 32 36 eqtrd 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> b = ( Base ` R ) )
38 37 6 eqtr4di 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> b = B )
39 simp2 
 |-  ( ( u = U /\ b = B /\ m = M ) -> b = B )
40 simp1 
 |-  ( ( u = U /\ b = B /\ m = M ) -> u = U )
41 40 fveq2d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( Base ` u ) = ( Base ` U ) )
42 41 3 eqtr4di 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( Base ` u ) = V )
43 simp3 
 |-  ( ( u = U /\ b = B /\ m = M ) -> m = M )
44 40 fveq2d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( .s ` u ) = ( .s ` U ) )
45 44 4 eqtr4di 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( .s ` u ) = .x. )
46 45 oveqd 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( x ( .s ` u ) v ) = ( x .x. v ) )
47 43 46 fveq12d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( m ` ( x ( .s ` u ) v ) ) = ( M ` ( x .x. v ) ) )
48 eqidd 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W ) )
49 48 7 eqtr4di 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( ( LCDual ` K ) ` W ) = C )
50 49 fveq2d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` C ) )
51 50 8 eqtr4di 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( .s ` ( ( LCDual ` K ) ` W ) ) = .xb )
52 eqidd 
 |-  ( ( u = U /\ b = B /\ m = M ) -> y = y )
53 43 fveq1d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( m ` v ) = ( M ` v ) )
54 51 52 53 oveq123d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) = ( y .xb ( M ` v ) ) )
55 47 54 eqeq12d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) <-> ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) )
56 42 55 raleqbidv 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) <-> A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) )
57 39 56 riotaeqbidv 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) = ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) )
58 39 57 mpteq12dv 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
59 58 eleq2d 
 |-  ( ( u = U /\ b = B /\ m = M ) -> ( a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) <-> a e. ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ) )
60 38 59 syld3an2 
 |-  ( ( u = U /\ b = ( Base ` ( Scalar ` u ) ) /\ m = M ) -> ( a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) <-> a e. ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ) )
61 29 30 31 60 sbc3ie 
 |-  ( [. U / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. M / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` W ) ) ( m ` v ) ) ) ) <-> a e. ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
62 28 61 bitrdi 
 |-  ( w = W -> ( [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) <-> a e. ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ) )
63 62 abbi1dv 
 |-  ( w = W -> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
64 eqid 
 |-  ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } )
65 63 64 6 mptfvmpt 
 |-  ( W e. H -> ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) ` W ) = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
66 14 65 sylan9eq 
 |-  ( ( K e. Y /\ W e. H ) -> I = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
67 11 66 syl 
 |-  ( ph -> I = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )