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=LHypK
Assertion hdmap1ffval KXHDMap1K=wHa|[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch

Proof

Step Hyp Ref Expression
1 hdmap1val.h H=LHypK
2 elex KXKV
3 fveq2 k=KLHypk=LHypK
4 3 1 eqtr4di k=KLHypk=H
5 fveq2 k=KDVecHk=DVecHK
6 5 fveq1d k=KDVecHkw=DVecHKw
7 fveq2 k=KLCDualk=LCDualK
8 7 fveq1d k=KLCDualkw=LCDualKw
9 fveq2 k=Kmapdk=mapdK
10 9 fveq1d k=Kmapdkw=mapdKw
11 10 sbceq1d k=K[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
12 11 sbcbidv k=K[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
13 12 sbcbidv k=K[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
14 8 13 sbceqbid k=K[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
15 14 sbcbidv k=K[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
16 15 sbcbidv k=K[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
17 6 16 sbceqbid k=K[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
18 17 abbidv k=Ka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch=a|[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
19 4 18 mpteq12dv k=KwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch=wHa|[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
20 df-hdmap1 HDMap1=kVwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
21 19 20 1 mptfvmpt KVHDMap1K=wHa|[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
22 2 21 syl KXHDMap1K=wHa|[˙DVecHKw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualKw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdKw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch