Metamath Proof Explorer


Theorem paddfval

Description: Projective subspace sum operation. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l ˙=K
paddfval.j ˙=joinK
paddfval.a A=AtomsK
paddfval.p +˙=+𝑃K
Assertion paddfval KB+˙=m𝒫A,n𝒫AmnpA|qmrnp˙q˙r

Proof

Step Hyp Ref Expression
1 paddfval.l ˙=K
2 paddfval.j ˙=joinK
3 paddfval.a A=AtomsK
4 paddfval.p +˙=+𝑃K
5 elex KBKV
6 fveq2 h=KAtomsh=AtomsK
7 6 3 eqtr4di h=KAtomsh=A
8 7 pweqd h=K𝒫Atomsh=𝒫A
9 eqidd h=Kp=p
10 fveq2 h=Kh=K
11 10 1 eqtr4di h=Kh=˙
12 fveq2 h=Kjoinh=joinK
13 12 2 eqtr4di h=Kjoinh=˙
14 13 oveqd h=Kqjoinhr=q˙r
15 9 11 14 breq123d h=Kphqjoinhrp˙q˙r
16 15 2rexbidv h=Kqmrnphqjoinhrqmrnp˙q˙r
17 7 16 rabeqbidv h=KpAtomsh|qmrnphqjoinhr=pA|qmrnp˙q˙r
18 17 uneq2d h=KmnpAtomsh|qmrnphqjoinhr=mnpA|qmrnp˙q˙r
19 8 8 18 mpoeq123dv h=Km𝒫Atomsh,n𝒫AtomshmnpAtomsh|qmrnphqjoinhr=m𝒫A,n𝒫AmnpA|qmrnp˙q˙r
20 df-padd +𝑃=hVm𝒫Atomsh,n𝒫AtomshmnpAtomsh|qmrnphqjoinhr
21 3 fvexi AV
22 21 pwex 𝒫AV
23 22 22 mpoex m𝒫A,n𝒫AmnpA|qmrnp˙q˙rV
24 19 20 23 fvmpt KV+𝑃K=m𝒫A,n𝒫AmnpA|qmrnp˙q˙r
25 4 24 eqtrid KV+˙=m𝒫A,n𝒫AmnpA|qmrnp˙q˙r
26 5 25 syl KB+˙=m𝒫A,n𝒫AmnpA|qmrnp˙q˙r