Theorem 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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cramerimp.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cramerimp.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	cramerimp.e	⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
	cramerimp.h	⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
	cramerimp.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	cramerimp.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	cramerimp.q	⊢ / = ( /r ‘ 𝑅 )
Assertion	cramerimp	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cramerimp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cramerimp.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cramerimp.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4		cramerimp.e	⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
5		cramerimp.h	⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
6		cramerimp.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
7		cramerimp.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
8		cramerimp.q	⊢ / = ( /r ‘ 𝑅 )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10	9	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ Ring )
11	10	3ad2ant1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13	7 1 2 12	mdetf	⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
14	13	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
15	14	3ad2ant1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
16	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
17	16	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
18	17	adantr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
19	10 18	anim12i	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
20	19	3adant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
21		ne0i	⊢ ( 𝐼 ∈ 𝑁 → 𝑁 ≠ ∅ )
22	9 21	anim12ci	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) )
23	22	anim1i	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
24	23	3adant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
25		simpl	⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
26	25	3ad2ant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
27	1 2 3 6	slesolvec	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
28	24 26 27	sylc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑍 ∈ 𝑉 )
29		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
30	29	3ad2ant1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐼 ∈ 𝑁 )
31		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
32	1 2 3 31	ma1repvcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
33	20 28 30 32	syl12anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
34	4 33	eqeltrid	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐸 ∈ 𝐵 )
35	15 34	ffvelcdmd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) )
36		simpr	⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
37	36	3ad2ant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
38		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
39		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
40	12 38 8 39	dvrcan3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝐸 ) )
41	11 35 37 40	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝐸 ) )
42		simpl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ CRing )
43	42	3ad2ant1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ CRing )
44	12 38	unitcl	⊢ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
45	44	adantl	⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
46	45	3ad2ant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
47	12 39	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) )
48	43 35 46 47	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) )
49	48	oveq1d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
50	18	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑁 ∈ Fin )
51	42	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑅 ∈ CRing )
52	29	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑁 )
53	50 51 52	3jca	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) )
54	53	3adant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) )
55	1 3 4 7	cramerimplem1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑍 ‘ 𝐼 ) )
56	54 28 55	syl2anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑍 ‘ 𝐼 ) )
57	41 49 56	3eqtr3rd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
58	1 2 3 4 5 6 7 39	cramerimplem3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) = ( 𝐷 ‘ 𝐻 ) )
59	58	3adant3r	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) = ( 𝐷 ‘ 𝐻 ) )
60	59	oveq1d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )
61	57 60	eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )