slesolinv

Description: The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 10-Feb-2019) (Revised by AV, 28-Feb-2019)

	Ref	Expression
Hypotheses	slesolex.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑_m 𝑁 )
	slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	slesolex.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	slesolinv.i	⊢ 𝐼 = ( inv_r ‘ 𝐴 )
Assertion	slesolinv	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		slesolex.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑_m 𝑁 )
4		slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
5		slesolex.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
6		slesolinv.i	⊢ 𝐼 = ( inv_r ‘ 𝐴 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9	8	adantl	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
10	9	3ad2ant1	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑅 ∈ Ring )
11	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
12	11	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
13	12	adantr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
14	13	3ad2ant2	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑁 ∈ Fin )
15	8	anim2i	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) )
16	15	anim1i	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
17	16	3adant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
18		simpr	⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
19	18	3ad2ant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
20	1 2 3 4	slesolvec	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
21	17 19 20	sylc	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 ∈ 𝑉 )
22	21 3	eleqtrdi	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑_m 𝑁 ) )
23		eqid	⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
24	9 13	anim12ci	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
25	24	3adant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
26	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
27	25 26	syl	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝐴 ∈ Ring )
28		eqid	⊢ ( Unit ‘ 𝐴 ) = ( Unit ‘ 𝐴 )
29		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
30	1 5 2 28 29	matunit	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( Unit ‘ 𝐴 ) ↔ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
31	30	bicomd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ↔ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
32	31	ad2ant2lr	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ↔ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
33	32	biimpd	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) → 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
34	33	adantrd	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
35	34	3impia	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑋 ∈ ( Unit ‘ 𝐴 ) )
36		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
37	28 6 36	ringinvcl	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
38	27 35 37	syl2anc	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
39	2	eleq2i	⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
40	39	birani	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
41	40	3ad2ant2	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
42	1 7 4 10 14 22 23 38 41	mavmulass	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( ( 𝐼 ‘ 𝑋 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑋 ) · 𝑍 ) = ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑍 ) ) )
43		simpr	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
44	43 13	anim12ci	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
45	44	3adant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
46	1 23	matmulr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( ._r ‘ 𝐴 ) )
47	45 46	syl	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( ._r ‘ 𝐴 ) )
48	47	oveqd	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑋 ) = ( ( 𝐼 ‘ 𝑋 ) ( ._r ‘ 𝐴 ) 𝑋 ) )
49		eqid	⊢ ( ._r ‘ 𝐴 ) = ( ._r ‘ 𝐴 )
50		eqid	⊢ ( 1_r ‘ 𝐴 ) = ( 1_r ‘ 𝐴 )
51	28 6 49 50	unitlinv	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( ._r ‘ 𝐴 ) 𝑋 ) = ( 1_r ‘ 𝐴 ) )
52	27 35 51	syl2anc	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( ._r ‘ 𝐴 ) 𝑋 ) = ( 1_r ‘ 𝐴 ) )
53	48 52	eqtrd	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑋 ) = ( 1_r ‘ 𝐴 ) )
54	53	oveq1d	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( ( 𝐼 ‘ 𝑋 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑋 ) · 𝑍 ) = ( ( 1_r ‘ 𝐴 ) · 𝑍 ) )
55	1 7 4 10 14 22	1mavmul	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 1_r ‘ 𝐴 ) · 𝑍 ) = 𝑍 )
56	54 55	eqtrd	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( ( 𝐼 ‘ 𝑋 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑋 ) · 𝑍 ) = 𝑍 )
57		oveq2	⊢ ( ( 𝑋 · 𝑍 ) = 𝑌 → ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑍 ) ) = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )
58	57	adantl	⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑍 ) ) = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )
59	58	3ad2ant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑍 ) ) = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )
60	42 56 59	3eqtr3d	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )

Metamath Proof Explorer

Theorem slesolinv

Proof