# Metamath Proof Explorer

## Theorem hdmap1vallem

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (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.t
`|- ( ph -> T e. ( ( V X. D ) X. V ) )`
Assertion hdmap1vallem
`|- ( ph -> ( I ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) 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.t
` |-  ( ph -> T e. ( ( V X. D ) X. V ) )`
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmap1fval
` |-  ( ph -> I = ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) )`
17 16 fveq1d
` |-  ( ph -> ( I ` T ) = ( ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ` T ) )`
18 10 fvexi
` |-  Q e. _V`
19 riotaex
` |-  ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) e. _V`
20 18 19 ifex
` |-  if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) e. _V`
21 fveqeq2
` |-  ( x = T -> ( ( 2nd ` x ) = .0. <-> ( 2nd ` T ) = .0. ) )`
22 fveq2
` |-  ( x = T -> ( 2nd ` x ) = ( 2nd ` T ) )`
23 22 sneqd
` |-  ( x = T -> { ( 2nd ` x ) } = { ( 2nd ` T ) } )`
24 23 fveq2d
` |-  ( x = T -> ( N ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` T ) } ) )`
25 24 fveqeq2d
` |-  ( x = T -> ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) ) )`
26 2fveq3
` |-  ( x = T -> ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` T ) ) )`
27 26 22 oveq12d
` |-  ( x = T -> ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) )`
28 27 sneqd
` |-  ( x = T -> { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } )`
29 28 fveq2d
` |-  ( x = T -> ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) )`
30 29 fveq2d
` |-  ( x = T -> ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) )`
31 2fveq3
` |-  ( x = T -> ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` T ) ) )`
32 31 oveq1d
` |-  ( x = T -> ( ( 2nd ` ( 1st ` x ) ) R h ) = ( ( 2nd ` ( 1st ` T ) ) R h ) )`
33 32 sneqd
` |-  ( x = T -> { ( ( 2nd ` ( 1st ` x ) ) R h ) } = { ( ( 2nd ` ( 1st ` T ) ) R h ) } )`
34 33 fveq2d
` |-  ( x = T -> ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) )`
35 30 34 eqeq12d
` |-  ( x = T -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) <-> ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) )`
36 25 35 anbi12d
` |-  ( x = T -> ( ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) <-> ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) )`
37 36 riotabidv
` |-  ( x = T -> ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) )`
38 21 37 ifbieq2d
` |-  ( x = T -> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) )`
39 eqid
` |-  ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) = ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )`
40 38 39 fvmptg
` |-  ( ( T e. ( ( V X. D ) X. V ) /\ if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) e. _V ) -> ( ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) )`
41 15 20 40 sylancl
` |-  ( ph -> ( ( x e. ( ( V X. D ) X. V ) |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) )`
42 17 41 eqtrd
` |-  ( ph -> ( I ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) .- ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) )`