Proof of an Optimal substructure in Dynammic Programming?
There is no (one) formal definition of "optimal substructure" (or the Bellman optimality criterion) so you can not possibly hope to (formally) prove you have it.

You should do the following:


Set up your (candidate) dynamic programming recurrence.
Prove it correct by induction.
Formulate the (iterative, memoizing) algorithm following the recurrence.