---

Step * of Lemma fps-elim-div

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[z:|r|]. ∀[x:X].
    (fps-elim(x) (f÷g)) = (fps-elim(x) f÷fps-elim(x) g) ∈ PowerSeries(X;r) 
    supposing (¬((fps-elim(x) f) = 0 ∈ PowerSeries(X;r))) ∧ ((g[{}] * z) = 1 ∈ |r|) 
  supposing valueall-type(X)
BY
{ (xxxInstLemma `fps-div-property` []xxx
   THEN RepeatFor 7 (ParallelLast')
   THEN Auto
   THEN (Assert (fps-elim(x) (g*(f÷g))) = (fps-elim(x) f) ∈ PowerSeries(X;r) BY
               Auto)
   THEN InstLemma `fps-elim-hom` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜x⌝]⋅
   THEN Auto
   THEN ((RepUR ``fun_thru_2op`` (-2) THEN RWO "-2" (-4)) THEN Auto)
   THEN InstLemma `fps-div-unique` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜fps-elim(x) f⌝;⌜fps-elim(x) g⌝;⌜z⌝;⌜fps-elim(x) (f÷g)⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].  \mforall{}[z:|r|].  \mforall{}[x:X].
        (fps-elim(x)  (f\mdiv{}g))  =  (fps-elim(x)  f\mdiv{}fps-elim(x)  g) 
        supposing  (\mneg{}((fps-elim(x)  f)  =  0))  \mwedge{}  ((g[\{\}]  *  z)  =  1) 
    supposing  valueall-type(X)


By

---

Latex:
(xxxInstLemma  `fps-div-property`  []xxx
  THEN  RepeatFor  7  (ParallelLast')
  THEN  Auto
  THEN  (Assert  (fps-elim(x)  (g*(f\mdiv{}g)))  =  (fps-elim(x)  f)  BY
                          Auto)
  THEN  InstLemma  `fps-elim-hom`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ((RepUR  ``fun\_thru\_2op``  (-2)  THEN  RWO  "-2"  (-4))  THEN  Auto)
  THEN  InstLemma  `fps-div-unique`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}fps-elim(x)  f\mkleeneclose{};\mkleeneopen{}fps-elim(x)  g\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}fps-elim(x) 
                                                                                                                                                                        (f\mdiv{}g)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index