Cramer's Rule (Metamath 100 #97)

[metamath]

Cramer's Rule (Metamath 100 #97)

[avekens]

I just posted a pull request containg a proof of Cramer's rule (~ cramer ) and other theorems for matrices and their determinants. Fortunately, it was not so difficult to prove Cramer's rule as expected. The special case of the Laplace Expansion I already proved (~ smadiadet ) was sufficient for it. And I could use again a lot of theorems from SO's determinants-1 branch. @sorear: Again, thank you very, very much for your magnificent work!

@david-a-wheeler: may I ask you to update the 100 theorems list and inform Freek again?
If http://www.cs.ru.nl/%7Efreek/100/ is up-to-date, then we will really move up to place 3 and overtake Mizar and Coq! Maybe Stefan can also be mentioned as contributor, because without his preliminary work I would'nt have been able to proof Cramer's rule.

Also many thanks to Norm and Mario for their valuable hints and support, and also to David "pushing" me/us to prove another theorem of the 100 theorem list.

To reach this goal, I had to hurry up a little bit, so there are many (known and unknown) imperfections
in my contribution (e.g. an appropriate definition for "column vectors" and "systems of linear equations"). I would be thankful for any hints and remarks.

[sorear]

(the plan was permutations → determinants → cayley-hamilton → algebraic numbers are a field → ??? → lindemann-weierstrass → pi e/ AA, but I haven't made much time for this lately)

[david-a-wheeler]

Note that we have a separate issue for proving the Lindemann–Weierstrass theorem (metamath 100 #56).

[david-a-wheeler]

@sorear - you've already basically done determinants... can I convince you to prove Cramer's rule?

[david-a-wheeler]

@sorear - Any progress?

[avekens]

I wonder why this theorem is still not proven in Metamath yet! I had a look at the available definitions of matrices, matrix multiplication and determinants (in the Mathbox of Stefan O'Rear), and I think only the following two main theorems are missing (formal representation see below):

• Multiplicativity of the determinant (see ~ mdetmul below): det(X*Y) = det(X)*det(Y)
• Determinant of an invertible matrix (see ~ mdetinvn0 below): X e. ( Unit ` A ) <-> det(X)=/=0

${
mdetmul.d $e |- D = ( N maDet R ) $.
mdetmul.a $e |- A = ( N Mat R ) $.
mdetmul.b $e |- B = ( Base A ) $. mdetmul.m $e |- .X. = ( .r A ) $.
mdetmul.t $e |- .x. = ( .r R ) $. $( Multiplicativity of the determinant. ( Contributed by AV, 8-Dec-2018.) $) mdetmul $p |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> (D ( X .X. Y ) = ( D X ) .x. ( D Y ) $=
? $.
$}

${
mdetinvn0.d $e |- D = ( N maDet R ) $.
mdetinvn0.a $e |- A = ( N Mat R ) $.
mdetinvn0.b $e |- B = ( Base A ) $. mdetinvn0.z $e |- .0. = ( 0g R ) $.
$( The derminant of an invertible matrix is not 0. ( Contributed by AV,
8-Dec-2018.) $)
mdetinvn0 $p |- ( ( R e. CRing /\ X e. B )
-> ( X e. ( Unit A ) <-> ( D X ) =/= .0. ) ) $=
? $.
$}

Having this two theorems (and maybe a lot of auxiliary theorems) proved, I think Cramer's rule can be proven easily.

In addition, I want to make a suggestion how to formalize Cramer's rule. Here is my suggestion (together with one additional definition):

${
$d c i j l m n $.
$( Substitution of a column of a matrix by a vector. (Contributed by AV,
7-Dec-2018.) $)
df-matcsub $a |- matColSub = ( m e. _V , c e. _V
|-> ( l e. _V , n e. _V |-> ( i e. n , j e. n
|-> if ( j = c , ( i l { 0 } ) , ( i m j ) ) ) ) ) $.
$}

${
cramer.n $e |- N = ( 1 ... T ) $.
cramer.a $e |- A = ( N Mat R ) $.
cramer.f $e |- F = ( R freeLMod ( N X. { 1 } ) ) $.
cramer.d $e |- D = ( N maDet R ) $.
cramer.b $e |- B = ( Base A ) $. cramer.p $e |- P = ( Base F ) $.
cramer.m $e |- .X. = ( R maMul &lt;. N , N , { 1 } &gt;. ) $.
cramer.q $e |- ./ = ( /r ` R ) $.

$( Cramer's Rule (according to Wikipedia "Cramer's rule",
   ~ https://en.wikipedia.org/wiki/Cramer's_rule , 8-Dec-2018):
   "Consider a system of n linear equations for n unknowns, represented in
   matrix multiplication form as follows: A x = b where the n x n matrix A
   has a nonzero determinant, and the vector x = ( x_1 , ... , x_n )^T is
   the column vector of the variables. Then the theorem states that in this
   case the system has a unique solution, whose individual values for the
   unknowns are given by: x_i = det ( A_i ) / det ( A ) (i = 1 , ..., n)
   where A_i is the matrix formed by replacing the i-th column of A by the
   column vector b." In the following, L corresponds to the (column) vector
   b, X to the (column) vector x, and M to the matrix A. The matrix A_i is
   formally represented by ` ( L ( M matColSub i ) N ) `.  (Contributed by
   Alexander van der Vekens, 2-Dec-2018.) $)
cramer $p |- ( ( ( R e. CRing /\ T e. NN ) 
               /\ ( M e. B /\ M e. ( Unit ` A ) ) /\ ( X e. P /\ L e. P ) )
               -> ( ( M .X. X ) = L <-> A. i e. N ( X ` i ) 
                = ( ( D ` ( L ( M matColSub i ) N ) ) ./ ( D ` M ) ) ) ) $=
  ? $.

$}

However, I have some questions:

• As "index set" for the columns/lines of the matrices I use ( 1 ... T ). Alternatively, ( 0 ..^ T ) could be used. However, I think indices for matrices/column vectors are usually indexed starting with 1, so we do it, too. Any objections?
• Currently, there is no special definition/notation of a "column vector" in set.mm. Instead of defining it (and also the multiplication of a matrix with a column vector) I used nx1-matrices to represent the two column vectors in Cramer's rule. By this, Stefan`s general matrix multiplication ~ df-mamu (and many available theorems for it) can be used. Is this OK?
• would it be sufficient to show the left-to-right-direction "->" of the theorem ( ( ( M .X. X ) = L -> A. i e. N ( X i ) = ( ( D ( L ( M matColSub i ) N ) ) ./ ( D M ) ) )) to "prove" Cramer's rule? Or is the right-to-left-direction "<-" ( A. i e. N ( X i ) = ( ( D ( L ( M matColSub i ) N ) ) ./ ( D M ) ) )-> ( M .X. X ) = L ) also required? I currently do not even know if this is easy to prove or provable at all...

Hints:

• M e. ( Unit ` A ) -> M e. B (see ~ unitcl )

If we can agree on this formalization of Cramer's rule, we maybe can proof it as a joint action: If sombody wants to proof ~ mdetmul and/or ~ mdetinvn0 , I will try the rest...

Regards,
Alexander

[david-a-wheeler]

On December 8, 2018 3:51:56 AM EST, avekens ***@***.***> wrote: I wonder why this theorem is still not proven in Metamath yet!

Please prove it! Metamath skips beyond 2 other provers with 1 more proof.

…

--- David A.Wheeler

[sorear]

see the determinants-1 branch I just pushed for a formalization of mdetmul which I did back in June; I haven't had cycles recently (major personal issues) to clean this up and get it in, but if someone else wants to look at it or I can try to get that done later this month

[avekens]

Wow, very impressive what I found in the determinants-1 branch. And it contains already the theorem mdetmul I requested. However, its proof has about 500 step, so it will take a while until I understand it. Unfortunately, there are no comments for the new therorems...
Nevertheless, with this material we are a great step further in direction of proving Cramer's rule.

[avekens]

@sorear: by looking at the determinants-1 branch, I recognized that you used two (slightly) different definitions of a determinant:

• in branches master/develop: df-mdet $a |- maDet = ( n e. _V , r e. _V |-> ( m e. ( Base `` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base `` ( SymGrp `` n ) ) |-> ( ( ( ZRHom `` r ) `` ( ( pmSgn `` n ) `` p ) ) ( .r `` r ) ( ( mulGrp `` r ) gsum ( x e. n |-> ( ( p `` x ) m x ) ) ) ) ) ) ) ) $.

• in branch determinants-1: df-mdet $a |- maDet = ( n e. _V , r e. _V |-> ( m e. ( Base `` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base `` ( SymGrp `` n ) ) |-> ( ( ( ( ZRHom `` r ) o. ( pmSgn `` n ) ) `` p ) ( .r `` r ) ( ( mulGrp `` r ) gsum ( x e. n |-> ( ( p `` x ) m x ) ) ) ) ) ) ) ) $.

These definitions are not equivalent, because ( ( ZRHom `` r ) `` ( ( pmSgn `` n ) `` p ) ) does not always equal ( ( ( ZRHom `` r ) o. ( pmSgn `` n ) ) `` p ). However, if n e. Fin, the definitions would be equivalent.

Question (maybe to everybody): Which definition is best/should be used? The theorems I contributed in my Mathbox are based on the first definition, of course.

[avekens]

OK, I think the second definition is the better oine, because if p e/ dom ( pmSgn `` n ). then ( ( ZRHom `` r ) `` ( ( pmSgn `` n ) `` p ) ) = ( ( ZRHom `` r ) `` (/) ) is not defined, but ( ( ( ZRHom r ) o. ( pmSgn n ) ) `` p ) = (/)`. To update the (one) theorem in my Mathbox directly depending on this definition is not difficult...

Does everybody agree to use the definition from branch determinants-1?.

[digama0]

Do we care about the case when p e/ dom ( pmSgn ` n )? From the definition it looks like this only happens when p is not a finitely supported permutation, which only happens when n is infinite. But then n Mat r is undefined. So it doesn't matter, and the two definitions are provably equal.

[avekens]

@digama0: You're right, thanks a lot for this hint. By this, I could prove that the two definitions are equal, so we can choose any of them and derive the other.

[avekens]

Status end of 2018:

I am experimenting with the definitions and theorems for determinants and related constructs for some weeks now, and I think there are two major issues on the way to proof Cramer's rule:

1. It is very difficult to get an overview of all the existing material and to prove new theorems in the current situation (all relevant definitions and theorems are contained in SO's Mathbox or, even worse, in his branch "determinants-1". And both contain (slightly) different definitions of the determinant of a square matrix). Because of this, I would propose to consolidate the material first.

• At least the theorems of the branch should be moved into the main branches (master/develop), and the definitions should be aligned there (definition from the branch is preferred, see previous discussions).
  @sorear: Maybe you can do this first. If you get any errors in my Mathbox (and you will if you take the definition from the branch), please comment out the erroneous proofs/theorems (I hope this will be only one theorem, ~ m2detleib ) - I will take care of them later.

• But maybe the corresponding sections could be moved right to the main part of set.mm (Maybe as section 10.13 titled. "Matrices and determinants" - it must be located at least after 10.11, because the definition of ZRHom is required). The following subsections (from SO's Mathbox) should be moved into this new section:
  19.17.43 Direct sum of left modules cdsmm 28017
  1917.44 Free modules cfrlm 28032
  19.17.54 Words in monoids and ordered group sum issubmd 28203
  19.17.55 Transpositions in the symmetric group cpmtr 28204
  19.17.56 The sign of a permutation cpsgn 28234
  19.17.57 The matrix algebra cmmul 28259
  19.17.58 The determinant cmdat 28303
  However, I do not know how much is required of the other subsections (19.17.1-42 and 19.17.45-53) - maybe Stefan can give a hint.

• A compromise could be to create a "topic Mathbox" with these subsections. Then Stefan and I can put our material into it and can continue working in this mathbox. This could be moved to the main part later, then.

2. To proof Cramer's rule, I think we have to prove the Laplace expansion of a determinant first. However, this seems not to be easy, because the current definitions of matrices and determinants use arbitrary finite sets N as index sets, not sequential integer ranges ( 1 ... n ) as usual. It's impressing what can be proven with this more general definition, but I have no clue how to prove (or even formulate) the Laplace expansion on this basis. Does anybody has an idea for this? If there is no other way, we need to restrict ourselves to sequential integer ranges for the Laplace expansion as well as for Cramer's rule. But even then, I guess it will be a lot of work to do.

@david-a-wheeler: Sorry, David, that I gave hope that by proving Cramer's rule we could make a quick progress concerning the 100 theorem list. But maybe its only me who is "blocked", and somebody else sees an easy way to prove Cramer's rule quickly.

[avekens]

Since Cramer's rule is proven now, this issue can be closed. As a follow-up, issue #769 is created to move the results from the Mathboxes into the main part of set.mm.

[avekens]

@david-a-wheeler could you close this issue, please? I cannot do it (only the creator of an issue can close it?).

[david-a-wheeler]

With pleasure!!!