cramerimplem1

Description: Lemma 1 for cramerimp : The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019) (Revised by AV, 5-Jul-2022)

	Ref	Expression
Hypotheses	cramerimplem1.a	$⊢ A = N Mat R$
	cramerimplem1.v	$⊢ V = {Base}_{R}^{N}$
	cramerimplem1.e	$⊢ E = (1_{A} (N matRepV R) Z) (I)$
	cramerimplem1.d	$⊢ D = N maDet R$
Assertion	cramerimplem1	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (E) = Z (I)$

Proof

Step	Hyp	Ref	Expression
1		cramerimplem1.a	$⊢ A = N Mat R$
2		cramerimplem1.v	$⊢ V = {Base}_{R}^{N}$
3		cramerimplem1.e	$⊢ E = (1_{A} (N matRepV R) Z) (I)$
4		cramerimplem1.d	$⊢ D = N maDet R$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	5	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
7	6	ancomd	$⊢ (N \in Fin \land R \in CRing) \to (R \in Ring \land N \in Fin)$
8	7	3adant3	$⊢ (N \in Fin \land R \in CRing \land I \in N) \to (R \in Ring \land N \in Fin)$
9		simp3	$⊢ (N \in Fin \land R \in CRing \land I \in N) \to I \in N$
10	9	anim1i	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to (I \in N \land Z \in V)$
11	1	fveq2i	$⊢ 1_{A} = 1_{(N Mat R)}$
12	2 11 3	1marepvmarrepid	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (E (N matRRep R) Z (I)) I = E$
13	8 10 12	syl2an2r	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to I (E (N matRRep R) Z (I)) I = E$
14	13	eqcomd	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to E = I (E (N matRRep R) Z (I)) I$
15	14	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (E) = D (I (E (N matRRep R) Z (I)) I)$
16	4	a1i	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D = N maDet R$
17	16	fveq1d	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (I (E (N matRRep R) Z (I)) I) = (N maDet R) (I (E (N matRRep R) Z (I)) I)$
18		simpl2	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to R \in CRing$
19	9	anim1ci	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to (Z \in V \land I \in N)$
20	1	eqcomi	$⊢ N Mat R = A$
21	20	fveq2i	$⊢ {Base}_{(N Mat R)} = {Base}_{A}$
22		eqid	$⊢ 1_{A} = 1_{A}$
23	1 21 2 22	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 {Base}_{(N Mat R)}$
24	8 19 23	syl2an2r	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to (1_{A} (N matRepV R) Z) (I) \in {Base}_{(N Mat R)}$
25	3 24	eqeltrid	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to E \in {Base}_{(N Mat R)}$
26	9	adantr	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to I \in N$
27		elmapi	$⊢ Z \in ({Base}_{R}^{N}) \to Z : N ⟶ {Base}_{R}$
28		ffvelcdm	$⊢ (Z : N ⟶ {Base}_{R} \land I \in N) \to Z (I) \in {Base}_{R}$
29	28	ex	$⊢ Z : N ⟶ {Base}_{R} \to (I \in N \to Z (I) \in {Base}_{R})$
30	27 29	syl	$⊢ Z \in ({Base}_{R}^{N}) \to (I \in N \to Z (I) \in {Base}_{R})$
31	30 2	eleq2s	$⊢ Z \in V \to (I \in N \to Z (I) \in {Base}_{R})$
32	31	com12	$⊢ I \in N \to (Z \in V \to Z (I) \in {Base}_{R})$
33	32	3ad2ant3	$⊢ (N \in Fin \land R \in CRing \land I \in N) \to (Z \in V \to Z (I) \in {Base}_{R})$
34	33	imp	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to Z (I) \in {Base}_{R}$
35		smadiadetr	$⊢ ((R \in CRing \land E \in {Base}_{(N Mat R)}) \land (I \in N \land Z (I) \in {Base}_{R})) \to (N maDet R) (I (E (N matRRep R) Z (I)) I) = Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I)$
36	18 25 26 34 35	syl22anc	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to (N maDet R) (I (E (N matRRep R) Z (I)) I) = Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I)$
37	17 36	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (I (E (N matRRep R) Z (I)) I) = Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I)$
38	2 11 3	1marepvsma1	$⊢ ((R \in Ring \land N \in Fin) \land (I \in N \land Z \in V)) \to I (N subMat R) (E) I = 1_{((N ∖ \{I\}) Mat R)}$
39	8 10 38	syl2an2r	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to I (N subMat R) (E) I = 1_{((N ∖ \{I\}) Mat R)}$
40	39	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I) = ((N ∖ \{I\}) maDet R) (1_{((N ∖ \{I\}) Mat R)})$
41	40	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I) = Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (1_{((N ∖ \{I\}) Mat R)})$
42		diffi	$⊢ N \in Fin \to N ∖ \{I\} \in Fin$
43	42	anim1ci	$⊢ (N \in Fin \land R \in CRing) \to (R \in CRing \land N ∖ \{I\} \in Fin)$
44	43	3adant3	$⊢ (N \in Fin \land R \in CRing \land I \in N) \to (R \in CRing \land N ∖ \{I\} \in Fin)$
45	44	adantr	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to (R \in CRing \land N ∖ \{I\} \in Fin)$
46		eqid	$⊢ (N ∖ \{I\}) maDet R = (N ∖ \{I\}) maDet R$
47		eqid	$⊢ (N ∖ \{I\}) Mat R = (N ∖ \{I\}) Mat R$
48		eqid	$⊢ 1_{((N ∖ \{I\}) Mat R)} = 1_{((N ∖ \{I\}) Mat R)}$
49		eqid	$⊢ 1_{R} = 1_{R}$
50	46 47 48 49	mdet1	$⊢ (R \in CRing \land N ∖ \{I\} \in Fin) \to ((N ∖ \{I\}) maDet R) (1_{((N ∖ \{I\}) Mat R)}) = 1_{R}$
51	45 50	syl	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to ((N ∖ \{I\}) maDet R) (1_{((N ∖ \{I\}) Mat R)}) = 1_{R}$
52	51	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (1_{((N ∖ \{I\}) Mat R)}) = Z (I) \cdot_{R} 1_{R}$
53	5	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land I \in N) \to R \in Ring$
54		eqid	$⊢ {Base}_{R} = {Base}_{R}$
55		eqid	$⊢ \cdot_{R} = \cdot_{R}$
56	54 55 49	ringridm	$⊢ (R \in Ring \land Z (I) \in {Base}_{R}) \to Z (I) \cdot_{R} 1_{R} = Z (I)$
57	53 34 56	syl2an2r	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to Z (I) \cdot_{R} 1_{R} = Z (I)$
58	41 52 57	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to Z (I) \cdot_{R} ((N ∖ \{I\}) maDet R) (I (N subMat R) (E) I) = Z (I)$
59	15 37 58	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land I \in N) \land Z \in V) \to D (E) = Z (I)$

Metamath Proof Explorer

Theorem cramerimplem1

Proof