Note that it is necessary that all of the equations in the spreadsheet have solutions, since they are implied by the original equations. The equations involving only knowns play a key role. In particular, they say precisely that, there must exist a projection such that
The converse is also true and can be verified with the assistance of the above spreadsheet. To do this, we assume that the matrices A, B, C and are given and that (theTwoEquations) holds, and wish to define , , , , a, b, c, e, f and g such that each of the equations in the above spreadsheet hold. If we can do this, then each of the equations from the starting polynomial equations (FAC) given in §subsection:problem will hold and we will have shown that a minimal factorization of the [A,B,C,1] system exists.
With the assignments made above, every equation in the spreadsheet above holds. Thus, by backsolving through the spreadsheet, we have constructed the factors of the original system [A,B,C,1]. This proves
Theorem ([BGKvD]) The system [A, B, C, 1] can be factored if and only if there exists a projection such that and .
Note that the known equations can be neatly expressed in terms of and . Indeed, it is easy to check with a little algebra that these are equivalent to (eq:answer). It is a question of taste, not algebra, as to which form one chooses.
For a more complicated example of an end game, see §.