weblib/ricciott/prova.ma

   1 include "basics/pts.ma".
   2
   3 axiom R : Type[0].
   4 axiom V : Type[0].
   5
   6 axiom f : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
   7
   8 axiom rplus : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
   9 axiom rtimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
  10
  11 axiom vplus : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
  12 axiom stimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
  13
  14 interpretation "real plus" 'plus x y = (rplus x y).
  15 interpretation "real times" 'times x y = (rtimes x y).
  16
  17 interpretation "vector plus" 'plus x y = (vplus x y).
  18 interpretation "scalar product on vectors" 'times x y = (stimes x y).
  19
  20 axiom a : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6. axiom b : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
  21 axiom x : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom y : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom z : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
  22
  23 include "basics/logic.ma".
  24
  25 axiom fa : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 -> \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
  26
  27 lemma pippo : \ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 (\ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/z.dec"\ 6z\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6) \ 5a title="real plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/fa.dec"\ 6fa\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6) + z.