Metamath Proof Explorer


Theorem hdmap1ffval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015)

Ref Expression
Hypothesis hdmap1val.h H = LHyp K
Assertion hdmap1ffval K X HDMap1 K = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h

Proof

Step Hyp Ref Expression
1 hdmap1val.h H = LHyp K
2 elex K X K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 syl6eqr k = K LHyp k = H
5 fveq2 k = K DVecH k = DVecH K
6 5 fveq1d k = K DVecH k w = DVecH K w
7 fveq2 k = K LCDual k = LCDual K
8 7 fveq1d k = K LCDual k w = LCDual K w
9 fveq2 k = K mapd k = mapd K
10 9 fveq1d k = K mapd k w = mapd K w
11 10 sbceq1d k = K [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
12 11 sbcbidv k = K [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
13 12 sbcbidv k = K [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
14 8 13 sbceqbid k = K [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
15 14 sbcbidv k = K [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
16 15 sbcbidv k = K [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
17 6 16 sbceqbid k = K [˙ DVecH k w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
18 17 abbidv k = K a | [˙ DVecH k w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
19 4 18 mpteq12dv k = K w LHyp k a | [˙ DVecH k w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
20 df-hdmap1 HDMap1 = k V w LHyp k a | [˙ DVecH k w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual k w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd k w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
21 19 20 1 mptfvmpt K V HDMap1 K = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
22 2 21 syl K X HDMap1 K = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h