Hello, I would like to apply matrix knowledge to the resolution of a system of two linear equations with two unknowns. So I have :

A * x + B * y + C = 0 and D * x + E * y + F = 0, and I know (x1, y1) such that the first left member is positive and the second one is 0, and (x2,y2) such that the first left member is negative and the second one is 0. I would like to prove that the system has a solution that is unique. I was thinking of using the matrix M that has A B D E as coefficient, show that because of the two witnesses this matrix is invertible, and just say the solution has to be A ^-1 *m V where V is the colon vector with C and F as coefficient.

I am already stuck at the objective of showing that my system of equations is the same as A *m X + F = 0. How can I expand the definition of matrix multiplication?

How does one use mulmx_key?

I think I found a solution: use matrixP and reason on each coefficient separately relying on mxE.

Here is a snippet (the function mkmx2 constructs a 2 by 2 matrix with the 4 coefficients, and the function mkcv2 is the same for a vector of dimension 2).

```
set M := mkmx2 A B D E.
set V1 := mkcv2 (b_x - a_x) (b_y - a_y).
set V2 := mkcv2 (d_x - c_x) (d_y - c_y).
have sys_to_mx_eqn :
forall x y, (A * x + B * y + C = 0 /\ D * x + E * y + F = 0) <->
(M *m (\col_(i < 2) if i == ord0 then x else y) +
(\col_(i < 2) if i == ord0 then C else F) = 0).
move=> x y; split.
move=> [eq1 eq2]; apply/matrixP=> i [ [ | j] jp] //; rewrite !mxE.
rewrite big_ord_recr /= big_ord1 /= !mxE /= {jp}.
by move: i=> [[ | [ | [ | i]]]].
move/matrixP=> mxeqn; split.
suff : A * x + B * y + C = 0 by [].
have := mxeqn (Ordinal (isT : (0 < 2)%N)) (Ordinal (isT : (0 < 1)%N)).
by rewrite !mxE /= big_ord_recr /= big_ord1 /= !mxE /=.
suff : D * x + E * y + F = 0 by [].
have := mxeqn (Ordinal (isT : (1 < 2)%N)) (Ordinal (isT : (0 < 1)%N)).
by rewrite !mxE /= big_ord_recr /= big_ord1 /= !mxE /=.
```

It may look long, but in fact there is a lot of repetition.

Would using `block_mx`

and `col_mx`

instead of custom `mkmx2`

and `mkcv2`

help?

I needed to have function that make it short to construct a matrix from the coefficients. The function `block_mx`

and `col_mx`

make it easier to build matrices from inputs that are already matrices.

By the way, I have solved my use case with two linear equations and two unknowns. It turns out that the determinant of the matrix M is a multiple of the difference of A * x + B * y + C at points (x1, y1) and (x2, y2). Unicity works well, but it is cumbersome that there is no existing theorem stating that multiplication by a unitmx is injective.

@Yves Bertot maybe using `mulrI`

( https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L2983 ) since matrix are equipped with a unitRingType.

@Pierre Roux , thanks for the suggestion, it does not work because I am multiplying by a matrix in `unitmx`

but left hand side and the right hand side are not in the same type (one type is `'M_2`

, the other is `'cV_2'), so I am not working in a unitRingType.

Does `can_inj`

/`can_eq`

together with `mulKmx`

/`mulmxK`

work? I can find several uses of these combinations in mathcomp.

Thanks @YAMAMOTO Mitsuharu , you are giving the right pointers: I should use mulKmx. Here is an example, with the following goal:

` M \in unitmx -> M *m V = V' -> V = M^-1 *m V'`

I can solve the goal with the following line:

`by move=> Munit solmv; rewrite -solmv mulKmx.`

If I don't already have the hypothesis `M *m V = V'`

, I can start with the following goal :

` M \in unitmx -> V = M^-1 *m V'`

and use the following tactic:

`move=>Munit; apply: (can_inj (mulKmx Munit)); rewrite mulKVmx.`

and end up with the following goal conclusion:

`M *m V = V'`

Alternatively,

`move=> Munit; apply: canRL (mulKmx Munit).`

and

`move=> Munit; apply: canRL (mulKmx Munit) _.`

,

respectively.

Last updated: Jan 29 2023 at 18:03 UTC