pinvmx
is the inverse of this isomporhism, but since the complement of the kernel that was used to produce pinvmx
is arbitrary, we must project the result of pinvmx
on S in order to get the specific inverse with image S.
Let E be a vector space (any dimension, but in Coq we reason in finite dimension).
Let u be an endomorphism of E, such that Ker u = Im u and S be a complement of Im u, so that E is the direct sum of S and Im u.
Show that for all x in E, there is a unique pair (y, z) in S² such that x = y + u (z), and pose v and z so that y = v(x) and z = w(x).
Instead of defining y and z for each x, we now define explicitly the matrix that computes y and z from x.
Note that we used locking in order to protect w and v from expanding unexpectedly during proofs.
Prove the following lemmas.
From the following lemma
Show some simplification lemmas
Indeed u (v x) + v (u x) = u (v x) + v (u (w x)) + v (u (u (v x))) by Su_rect = u (v x) + v (u (w x)) by u2K = u (v x) + w x by uv = x by -Su_rect
Indeed u (w x) + w (u x) = u (w x) + w (u (w x)) + w (u (u (v x))) by Su_rect = u (w x) + w (u (w x)) by u2K = u (w x) by uw = u (x - u (v x)) by Su_rect = u x by u2K
Let u be a endomorphism of E such that u^2 = 0.