cramerimp

Description: One direction of 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 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."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019) (Revised by AV, 1-Mar-2019)

	Ref	Expression
Hypotheses	cramerimp.a	$⊢ A = N Mat R$
	cramerimp.b	$⊢ B = {Base}_{A}$
	cramerimp.v	$⊢ V = {Base}_{R}^{N}$
	cramerimp.e	$⊢ E = (1_{A} (N matRepV R) Z) (I)$
	cramerimp.h	$⊢ H = (X (N matRepV R) Y) (I)$
	cramerimp.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	cramerimp.d	$⊢ D = N maDet R$
	cramerimp.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	cramerimp	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to Z (I) = D (H) \underset{˙}{\times} D (X)$

Proof

Step	Hyp	Ref	Expression
1		cramerimp.a	$⊢ A = N Mat R$
2		cramerimp.b	$⊢ B = {Base}_{A}$
3		cramerimp.v	$⊢ V = {Base}_{R}^{N}$
4		cramerimp.e	$⊢ E = (1_{A} (N matRepV R) Z) (I)$
5		cramerimp.h	$⊢ H = (X (N matRepV R) Y) (I)$
6		cramerimp.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
7		cramerimp.d	$⊢ D = N maDet R$
8		cramerimp.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	9	adantr	$⊢ (R \in CRing \land I \in N) \to R \in Ring$
11	10	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to R \in Ring$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	7 1 2 12	mdetf	$⊢ R \in CRing \to D : B ⟶ {Base}_{R}$
14	13	adantr	$⊢ (R \in CRing \land I \in N) \to D : B ⟶ {Base}_{R}$
15	14	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D : B ⟶ {Base}_{R}$
16	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
17	16	simpld	$⊢ X \in B \to N \in Fin$
18	17	adantr	$⊢ (X \in B \land Y \in V) \to N \in Fin$
19	10 18	anim12i	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to (R \in Ring \land N \in Fin)$
20	19	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (R \in Ring \land N \in Fin)$
21		ne0i	$⊢ I \in N \to N \neq \emptyset$
22	9 21	anim12ci	$⊢ (R \in CRing \land I \in N) \to (N \neq \emptyset \land R \in Ring)$
23	22	anim1i	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
24	23	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
25		simpl	$⊢ (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R)) \to X \underset{˙}{\cdot} Z = Y$
26	25	3ad2ant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to X \underset{˙}{\cdot} Z = Y$
27	1 2 3 6	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)$
28	24 26 27	sylc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to Z \in V$
29		simpr	$⊢ (R \in CRing \land I \in N) \to I \in N$
30	29	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to I \in N$
31		eqid	$⊢ 1_{A} = 1_{A}$
32	1 2 3 31	ma1repvcl	$⊢ ((R \in Ring \land N \in Fin) \land (Z \in V \land I \in N)) \to (1_{A} (N matRepV R) Z) (I) \in B$
33	20 28 30 32	syl12anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (1_{A} (N matRepV R) Z) (I) \in B$
34	4 33	eqeltrid	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to E \in B$
35	15 34	ffvelcdmd	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (E) \in {Base}_{R}$
36		simpr	$⊢ (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R)) \to D (X) \in Unit (R)$
37	36	3ad2ant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (X) \in Unit (R)$
38		eqid	$⊢ Unit (R) = Unit (R)$
39		eqid	$⊢ \cdot_{R} = \cdot_{R}$
40	12 38 8 39	dvrcan3	$⊢ (R \in Ring \land D (E) \in {Base}_{R} \land D (X) \in Unit (R)) \to (D (E) \cdot_{R} D (X)) \underset{˙}{\times} D (X) = D (E)$
41	11 35 37 40	syl3anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (D (E) \cdot_{R} D (X)) \underset{˙}{\times} D (X) = D (E)$
42		simpl	$⊢ (R \in CRing \land I \in N) \to R \in CRing$
43	42	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to R \in CRing$
44	12 38	unitcl	$⊢ D (X) \in Unit (R) \to D (X) \in {Base}_{R}$
45	44	adantl	$⊢ (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R)) \to D (X) \in {Base}_{R}$
46	45	3ad2ant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (X) \in {Base}_{R}$
47	12 39	crngcom	$⊢ (R \in CRing \land D (E) \in {Base}_{R} \land D (X) \in {Base}_{R}) \to D (E) \cdot_{R} D (X) = D (X) \cdot_{R} D (E)$
48	43 35 46 47	syl3anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (E) \cdot_{R} D (X) = D (X) \cdot_{R} D (E)$
49	48	oveq1d	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (D (E) \cdot_{R} D (X)) \underset{˙}{\times} D (X) = (D (X) \cdot_{R} D (E)) \underset{˙}{\times} D (X)$
50	18	adantl	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to N \in Fin$
51	42	adantr	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to R \in CRing$
52	29	adantr	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to I \in N$
53	50 51 52	3jca	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to (N \in Fin \land R \in CRing \land I \in N)$
54	53	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (N \in Fin \land R \in CRing \land I \in N)$
55	1 3 4 7	cramerimplem1	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (E) = Z (I)$
56	54 28 55	syl2anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (E) = Z (I)$
57	41 49 56	3eqtr3rd	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to Z (I) = (D (X) \cdot_{R} D (E)) \underset{˙}{\times} D (X)$
58	1 2 3 4 5 6 7 39	cramerimplem3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to D (X) \cdot_{R} D (E) = D (H)$
59	58	3adant3r	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to D (X) \cdot_{R} D (E) = D (H)$
60	59	oveq1d	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to (D (X) \cdot_{R} D (E)) \underset{˙}{\times} D (X) = D (H) \underset{˙}{\times} D (X)$
61	57 60	eqtrd	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to Z (I) = D (H) \underset{˙}{\times} D (X)$

Metamath Proof Explorer

Theorem cramerimp

Proof