cramerimplem2

Description: Lemma 2 for cramerimp : The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector 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.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
Assertion	cramerimplem2	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\times} E = H$

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.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		simpl	$⊢ (R \in CRing \land I \in N) \to R \in CRing$
11	10	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to R \in CRing$
12	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
13	12	simpld	$⊢ X \in B \to N \in Fin$
14	13	adantr	$⊢ (X \in B \land Y \in V) \to N \in Fin$
15	14	3ad2ant2	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to N \in Fin$
16	13	anim2i	$⊢ (R \in CRing \land X \in B) \to (R \in CRing \land N \in Fin)$
17	16	ancomd	$⊢ (R \in CRing \land X \in B) \to (N \in Fin \land R \in CRing)$
18	1 8	matbas2	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
19	17 18	syl	$⊢ (R \in CRing \land X \in B) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
20	2 19	eqtr4id	$⊢ (R \in CRing \land X \in B) \to B = {Base}_{R}^{(N \times N)}$
21	20	eleq2d	$⊢ (R \in CRing \land X \in B) \to (X \in B \leftrightarrow X \in ({Base}_{R}^{(N \times N)}))$
22	21	biimpd	$⊢ (R \in CRing \land X \in B) \to (X \in B \to X \in ({Base}_{R}^{(N \times N)}))$
23	22	ex	$⊢ R \in CRing \to (X \in B \to (X \in B \to X \in ({Base}_{R}^{(N \times N)})))$
24	23	adantr	$⊢ (R \in CRing \land I \in N) \to (X \in B \to (X \in B \to X \in ({Base}_{R}^{(N \times N)})))$
25	24	com12	$⊢ X \in B \to ((R \in CRing \land I \in N) \to (X \in B \to X \in ({Base}_{R}^{(N \times N)})))$
26	25	pm2.43a	$⊢ X \in B \to ((R \in CRing \land I \in N) \to X \in ({Base}_{R}^{(N \times N)}))$
27	26	adantr	$⊢ (X \in B \land Y \in V) \to ((R \in CRing \land I \in N) \to X \in ({Base}_{R}^{(N \times N)}))$
28	27	impcom	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to X \in ({Base}_{R}^{(N \times N)})$
29	28	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \in ({Base}_{R}^{(N \times N)})$
30		crngring	$⊢ R \in CRing \to R \in Ring$
31	30	adantr	$⊢ (R \in CRing \land I \in N) \to R \in Ring$
32	31 14	anim12i	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to (R \in Ring \land N \in Fin)$
33	32	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (R \in Ring \land N \in Fin)$
34		ne0i	$⊢ I \in N \to N \neq \emptyset$
35	34	adantl	$⊢ (R \in CRing \land I \in N) \to N \neq \emptyset$
36	35	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to N \neq \emptyset$
37	15 15 36	3jca	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (N \in Fin \land N \in Fin \land N \neq \emptyset)$
38	3	eleq2i	$⊢ Y \in V \leftrightarrow Y \in ({Base}_{R}^{N})$
39	38	biimpi	$⊢ Y \in V \to Y \in ({Base}_{R}^{N})$
40	39	adantl	$⊢ (X \in B \land Y \in V) \to Y \in ({Base}_{R}^{N})$
41	10 40	anim12i	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to (R \in CRing \land Y \in ({Base}_{R}^{N}))$
42	41	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (R \in CRing \land Y \in ({Base}_{R}^{N}))$
43		simp3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\cdot} Z = Y$
44		eqid	$⊢ {Base}_{R}^{(N \times N)} = {Base}_{R}^{(N \times N)}$
45		eqid	$⊢ {Base}_{R}^{N} = {Base}_{R}^{N}$
46	8 44 3 6 45	mavmulsolcl	$⊢ ((N \in Fin \land N \in Fin \land N \neq \emptyset) \land (R \in CRing \land Y \in ({Base}_{R}^{N}))) \to (X \underset{˙}{\cdot} Z = Y \to Z \in V)$
47	46	imp	$⊢ (((N \in Fin \land N \in Fin \land N \neq \emptyset) \land (R \in CRing \land Y \in ({Base}_{R}^{N}))) \land X \underset{˙}{\cdot} Z = Y) \to Z \in V$
48	37 42 43 47	syl21anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to Z \in V$
49		simpr	$⊢ (R \in CRing \land I \in N) \to I \in N$
50	49	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to I \in N$
51		eqid	$⊢ 1_{A} = 1_{A}$
52	1 2 3 51	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$
53	4 52	eqeltrid	$⊢ ((R \in Ring \land N \in Fin) \land (Z \in V \land I \in N)) \to E \in B$
54	33 48 50 53	syl12anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to E \in B$
55	20	eqcomd	$⊢ (R \in CRing \land X \in B) \to {Base}_{R}^{(N \times N)} = B$
56	55	ad2ant2r	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V)) \to {Base}_{R}^{(N \times N)} = B$
57	56	3adant3	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to {Base}_{R}^{(N \times N)} = B$
58	54 57	eleqtrrd	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to E \in ({Base}_{R}^{(N \times N)})$
59	7 8 9 11 15 15 15 29 58	mamuval	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\times} E = (i \in N, j \in N ⟼ \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l E j)))$
60	31	3ad2ant1	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to R \in Ring$
61	60	3ad2ant1	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to R \in Ring$
62		simpl	$⊢ (X \in B \land Y \in V) \to X \in B$
63	62	3ad2ant2	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \in B$
64	63 48 50	3jca	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (X \in B \land Z \in V \land I \in N)$
65	64	3ad2ant1	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to (X \in B \land Z \in V \land I \in N)$
66		simp2	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to i \in N$
67		simp3	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to j \in N$
68	43	3ad2ant1	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to X \underset{˙}{\cdot} Z = Y$
69		eqid	$⊢ 0_{R} = 0_{R}$
70	1 2 3 51 69 4 6	mulmarep1gsum2	$⊢ (R \in Ring \land (X \in B \land Z \in V \land I \in N) \land (i \in N \land j \in N \land X \underset{˙}{\cdot} Z = Y)) \to \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l E j)) = if (j = I, Y (i), i X j)$
71	61 65 66 67 68 70	syl113anc	$⊢ (((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \land i \in N \land j \in N) \to \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l E j)) = if (j = I, Y (i), i X j)$
72	71	mpoeq3dva	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (i \in N, j \in N ⟼ \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l E j))) = (i \in N, j \in N ⟼ if (j = I, Y (i), i X j))$
73		simpr	$⊢ (X \in B \land Y \in V) \to Y \in V$
74	73	3ad2ant2	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to Y \in V$
75		eqid	$⊢ N matRepV R = N matRepV R$
76	1 2 75 3	marepvval	$⊢ (X \in B \land Y \in V \land I \in N) \to (X (N matRepV R) Y) (I) = (i \in N, j \in N ⟼ if (j = I, Y (i), i X j))$
77	63 74 50 76	syl3anc	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (X (N matRepV R) Y) (I) = (i \in N, j \in N ⟼ if (j = I, Y (i), i X j))$
78	5 77	eqtr2id	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to (i \in N, j \in N ⟼ if (j = I, Y (i), i X j)) = H$
79	59 72 78	3eqtrd	$⊢ ((R \in CRing \land I \in N) \land (X \in B \land Y \in V) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\times} E = H$

Metamath Proof Explorer

Theorem cramerimplem2

Proof