Metamath Proof Explorer


Theorem djaffvalN

Description: Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis djaval.h H=LHypK
Assertion djaffvalN KVvAK=wHx𝒫LTrnKw,y𝒫LTrnKwocAKwocAKwxocAKwy

Proof

Step Hyp Ref Expression
1 djaval.h H=LHypK
2 elex KVKV
3 fveq2 k=KLHypk=LHypK
4 3 1 eqtr4di k=KLHypk=H
5 fveq2 k=KLTrnk=LTrnK
6 5 fveq1d k=KLTrnkw=LTrnKw
7 6 pweqd k=K𝒫LTrnkw=𝒫LTrnKw
8 fveq2 k=KocAk=ocAK
9 8 fveq1d k=KocAkw=ocAKw
10 9 fveq1d k=KocAkwx=ocAKwx
11 9 fveq1d k=KocAkwy=ocAKwy
12 10 11 ineq12d k=KocAkwxocAkwy=ocAKwxocAKwy
13 9 12 fveq12d k=KocAkwocAkwxocAkwy=ocAKwocAKwxocAKwy
14 7 7 13 mpoeq123dv k=Kx𝒫LTrnkw,y𝒫LTrnkwocAkwocAkwxocAkwy=x𝒫LTrnKw,y𝒫LTrnKwocAKwocAKwxocAKwy
15 4 14 mpteq12dv k=KwLHypkx𝒫LTrnkw,y𝒫LTrnkwocAkwocAkwxocAkwy=wHx𝒫LTrnKw,y𝒫LTrnKwocAKwocAKwxocAKwy
16 df-djaN vA=kVwLHypkx𝒫LTrnkw,y𝒫LTrnkwocAkwocAkwxocAkwy
17 15 16 1 mptfvmpt KVvAK=wHx𝒫LTrnKw,y𝒫LTrnKwocAKwocAKwxocAKwy
18 2 17 syl KVvAK=wHx𝒫LTrnKw,y𝒫LTrnKwocAKwocAKwxocAKwy