cramer

Description: Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule : "[Cramer's rule] ... expresses the [unique solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp ). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit or slesolinv . For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in Lang p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019) (Revised by Alexander van der Vekens, 1-Mar-2019)

	Ref	Expression
Hypotheses	cramer.a	$⊢ A = N Mat R$
	cramer.b	$⊢ B = {Base}_{A}$
	cramer.v	$⊢ V = {Base}_{R}^{N}$
	cramer.d	$⊢ D = N maDet R$
	cramer.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	cramer.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	cramer	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \leftrightarrow X \underset{˙}{\cdot} Z = Y)$

Proof

Step	Hyp	Ref	Expression
1		cramer.a	$⊢ A = N Mat R$
2		cramer.b	$⊢ B = {Base}_{A}$
3		cramer.v	$⊢ V = {Base}_{R}^{N}$
4		cramer.d	$⊢ D = N maDet R$
5		cramer.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
6		cramer.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
7		pm3.22	$⊢ (R \in CRing \land N \neq \emptyset) \to (N \neq \emptyset \land R \in CRing)$
8	1 2 3 4 5 6	cramerlem3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$
9	7 8	syl3an1	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$
10		simpl1l	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to R \in CRing$
11		simpl2	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to (X \in B \land Y \in V)$
12		simpl3	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to D (X) \in Unit (R)$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	13	anim1ci	$⊢ (R \in CRing \land N \neq \emptyset) \to (N \neq \emptyset \land R \in Ring)$
15	14	anim1i	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V)) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
16	15	3adant3	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
17	1 2 3 5	slesolvec	$⊢ ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V)) \to (X \underset{˙}{\cdot} Z = Y \to Z \in V)$
18	17	imp	$⊢ (((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V)) \land X \underset{˙}{\cdot} Z = Y) \to Z \in V$
19	16 18	sylan	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to Z \in V$
20		simpr	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\cdot} Z = Y$
21	1 2 3 4 5 6	cramerlem1	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
22	10 11 12 19 20 21	syl113anc	$⊢ (((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land X \underset{˙}{\cdot} Z = Y) \to Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
23	22	ex	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (X \underset{˙}{\cdot} Z = Y \to Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)))$
24	9 23	impbid	$⊢ ((R \in CRing \land N \neq \emptyset) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \leftrightarrow X \underset{˙}{\cdot} Z = Y)$

Metamath Proof Explorer

Theorem cramer

Proof