# Metamath Proof Explorer

## Theorem hdmap1val

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval .) TODO: change I = ( x e. _V |-> ... to ( ph -> ( I<. X , F , Y > ) = ... in e.g. mapdh8 to shorten proofs with no \$d on x . (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1val.h
`|- H = ( LHyp ` K )`
hdmap1fval.u
`|- U = ( ( DVecH ` K ) ` W )`
hdmap1fval.v
`|- V = ( Base ` U )`
hdmap1fval.s
`|- .- = ( -g ` U )`
hdmap1fval.o
`|- .0. = ( 0g ` U )`
hdmap1fval.n
`|- N = ( LSpan ` U )`
hdmap1fval.c
`|- C = ( ( LCDual ` K ) ` W )`
hdmap1fval.d
`|- D = ( Base ` C )`
hdmap1fval.r
`|- R = ( -g ` C )`
hdmap1fval.q
`|- Q = ( 0g ` C )`
hdmap1fval.j
`|- J = ( LSpan ` C )`
hdmap1fval.m
`|- M = ( ( mapd ` K ) ` W )`
hdmap1fval.i
`|- I = ( ( HDMap1 ` K ) ` W )`
hdmap1fval.k
`|- ( ph -> ( K e. A /\ W e. H ) )`
hdmap1val.x
`|- ( ph -> X e. V )`
hdmap1val.f
`|- ( ph -> F e. D )`
hdmap1val.y
`|- ( ph -> Y e. V )`
Assertion hdmap1val
`|- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )`

### Proof

Step Hyp Ref Expression
1 hdmap1val.h
` |-  H = ( LHyp ` K )`
2 hdmap1fval.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hdmap1fval.v
` |-  V = ( Base ` U )`
4 hdmap1fval.s
` |-  .- = ( -g ` U )`
5 hdmap1fval.o
` |-  .0. = ( 0g ` U )`
6 hdmap1fval.n
` |-  N = ( LSpan ` U )`
7 hdmap1fval.c
` |-  C = ( ( LCDual ` K ) ` W )`
8 hdmap1fval.d
` |-  D = ( Base ` C )`
9 hdmap1fval.r
` |-  R = ( -g ` C )`
10 hdmap1fval.q
` |-  Q = ( 0g ` C )`
11 hdmap1fval.j
` |-  J = ( LSpan ` C )`
12 hdmap1fval.m
` |-  M = ( ( mapd ` K ) ` W )`
13 hdmap1fval.i
` |-  I = ( ( HDMap1 ` K ) ` W )`
14 hdmap1fval.k
` |-  ( ph -> ( K e. A /\ W e. H ) )`
15 hdmap1val.x
` |-  ( ph -> X e. V )`
16 hdmap1val.f
` |-  ( ph -> F e. D )`
17 hdmap1val.y
` |-  ( ph -> Y e. V )`
18 df-ot
` |-  <. X , F , Y >. = <. <. X , F >. , Y >.`
19 opelxp
` |-  ( <. X , F >. e. ( V X. D ) <-> ( X e. V /\ F e. D ) )`
20 15 16 19 sylanbrc
` |-  ( ph -> <. X , F >. e. ( V X. D ) )`
21 opelxp
` |-  ( <. <. X , F >. , Y >. e. ( ( V X. D ) X. V ) <-> ( <. X , F >. e. ( V X. D ) /\ Y e. V ) )`
22 20 17 21 sylanbrc
` |-  ( ph -> <. <. X , F >. , Y >. e. ( ( V X. D ) X. V ) )`
23 18 22 eqeltrid
` |-  ( ph -> <. X , F , Y >. e. ( ( V X. D ) X. V ) )`
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 23 hdmap1vallem
` |-  ( ph -> ( I ` <. X , F , Y >. ) = if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) )`
25 ot3rdg
` |-  ( Y e. V -> ( 2nd ` <. X , F , Y >. ) = Y )`
26 17 25 syl
` |-  ( ph -> ( 2nd ` <. X , F , Y >. ) = Y )`
27 26 eqeq1d
` |-  ( ph -> ( ( 2nd ` <. X , F , Y >. ) = .0. <-> Y = .0. ) )`
28 26 sneqd
` |-  ( ph -> { ( 2nd ` <. X , F , Y >. ) } = { Y } )`
29 28 fveq2d
` |-  ( ph -> ( N ` { ( 2nd ` <. X , F , Y >. ) } ) = ( N ` { Y } ) )`
30 29 fveqeq2d
` |-  ( ph -> ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { Y } ) ) = ( J ` { h } ) ) )`
31 ot1stg
` |-  ( ( X e. V /\ F e. D /\ Y e. V ) -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )`
32 15 16 17 31 syl3anc
` |-  ( ph -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )`
33 32 26 oveq12d
` |-  ( ph -> ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) = ( X .- Y ) )`
34 33 sneqd
` |-  ( ph -> { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } = { ( X .- Y ) } )`
35 34 fveq2d
` |-  ( ph -> ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) = ( N ` { ( X .- Y ) } ) )`
36 35 fveq2d
` |-  ( ph -> ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( M ` ( N ` { ( X .- Y ) } ) ) )`
37 ot2ndg
` |-  ( ( X e. V /\ F e. D /\ Y e. V ) -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )`
38 15 16 17 37 syl3anc
` |-  ( ph -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )`
39 38 oveq1d
` |-  ( ph -> ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) = ( F R h ) )`
40 39 sneqd
` |-  ( ph -> { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } = { ( F R h ) } )`
41 40 fveq2d
` |-  ( ph -> ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) = ( J ` { ( F R h ) } ) )`
42 36 41 eqeq12d
` |-  ( ph -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) <-> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) )`
43 30 42 anbi12d
` |-  ( ph -> ( ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )`
44 43 riotabidv
` |-  ( ph -> ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )`
45 27 44 ifbieq2d
` |-  ( ph -> if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )`
46 24 45 eqtrd
` |-  ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )`