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	$⊢ A = N Mat R$
	slesolex.b	$⊢ B = {Base}_{A}$
	slesolex.v	$⊢ V = {Base}_{R}^{N}$
	slesolex.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	slesolex.d	$⊢ D = N maDet R$
	slesolinv.i	$⊢ I = {inv}_{r} (A)$
Assertion	slesolinv	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to Z = I (X) \underset{˙}{\cdot} Y$

Proof

Step	Hyp	Ref	Expression
1		slesolex.a	$⊢ A = N Mat R$
2		slesolex.b	$⊢ B = {Base}_{A}$
3		slesolex.v	$⊢ V = {Base}_{R}^{N}$
4		slesolex.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
5		slesolex.d	$⊢ D = N maDet R$
6		slesolinv.i	$⊢ I = {inv}_{r} (A)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		crngring	$⊢ R \in CRing \to R \in Ring$
9	8	adantl	$⊢ (N \neq \emptyset \land R \in CRing) \to R \in Ring$
10	9	3ad2ant1	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to R \in Ring$
11	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
12	11	simpld	$⊢ X \in B \to N \in Fin$
13	12	adantr	$⊢ (X \in B \land Y \in V) \to N \in Fin$
14	13	3ad2ant2	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to N \in Fin$
15	8	anim2i	$⊢ (N \neq \emptyset \land R \in CRing) \to (N \neq \emptyset \land R \in Ring)$
16	15	anim1i	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
17	16	3adant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V))$
18		simpr	$⊢ (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y) \to X \underset{˙}{\cdot} Z = Y$
19	18	3ad2ant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to X \underset{˙}{\cdot} Z = Y$
20	1 2 3 4	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)$
21	17 19 20	sylc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to Z \in V$
22	21 3	eleqtrdi	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to Z \in ({Base}_{R}^{N})$
23		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
24	9 13	anim12ci	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (N \in Fin \land R \in Ring)$
25	24	3adant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to (N \in Fin \land R \in Ring)$
26	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
27	25 26	syl	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to A \in Ring$
28		eqid	$⊢ Unit (A) = Unit (A)$
29		eqid	$⊢ Unit (R) = Unit (R)$
30	1 5 2 28 29	matunit	$⊢ (R \in CRing \land X \in B) \to (X \in Unit (A) \leftrightarrow D (X) \in Unit (R))$
31	30	bicomd	$⊢ (R \in CRing \land X \in B) \to (D (X) \in Unit (R) \leftrightarrow X \in Unit (A))$
32	31	ad2ant2lr	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (D (X) \in Unit (R) \leftrightarrow X \in Unit (A))$
33	32	biimpd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (D (X) \in Unit (R) \to X \in Unit (A))$
34	33	adantrd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to ((D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y) \to X \in Unit (A))$
35	34	3impia	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to X \in Unit (A)$
36		eqid	$⊢ {Base}_{A} = {Base}_{A}$
37	28 6 36	ringinvcl	$⊢ (A \in Ring \land X \in Unit (A)) \to I (X) \in {Base}_{A}$
38	27 35 37	syl2anc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to I (X) \in {Base}_{A}$
39	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
40	39	birani	$⊢ (X \in B \land Y \in V) \to X \in {Base}_{A}$
41	40	3ad2ant2	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to X \in {Base}_{A}$
42	1 7 4 10 14 22 23 38 41	mavmulass	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to (I (X) (R maMul ⟨N, N, N⟩) X) \underset{˙}{\cdot} Z = I (X) \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$
43		simpr	$⊢ (N \neq \emptyset \land R \in CRing) \to R \in CRing$
44	43 13	anim12ci	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (N \in Fin \land R \in CRing)$
45	44	3adant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to (N \in Fin \land R \in CRing)$
46	1 23	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
47	45 46	syl	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
48	47	oveqd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to I (X) (R maMul ⟨N, N, N⟩) X = I (X) \cdot_{A} X$
49		eqid	$⊢ \cdot_{A} = \cdot_{A}$
50		eqid	$⊢ 1_{A} = 1_{A}$
51	28 6 49 50	unitlinv	$⊢ (A \in Ring \land X \in Unit (A)) \to I (X) \cdot_{A} X = 1_{A}$
52	27 35 51	syl2anc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to I (X) \cdot_{A} X = 1_{A}$
53	48 52	eqtrd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to I (X) (R maMul ⟨N, N, N⟩) X = 1_{A}$
54	53	oveq1d	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to (I (X) (R maMul ⟨N, N, N⟩) X) \underset{˙}{\cdot} Z = 1_{A} \underset{˙}{\cdot} Z$
55	1 7 4 10 14 22	1mavmul	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to 1_{A} \underset{˙}{\cdot} Z = Z$
56	54 55	eqtrd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to (I (X) (R maMul ⟨N, N, N⟩) X) \underset{˙}{\cdot} Z = Z$
57		oveq2	$⊢ X \underset{˙}{\cdot} Z = Y \to I (X) \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z) = I (X) \underset{˙}{\cdot} Y$
58	57	adantl	$⊢ (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y) \to I (X) \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z) = I (X) \underset{˙}{\cdot} Y$
59	58	3ad2ant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to I (X) \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z) = I (X) \underset{˙}{\cdot} Y$
60	42 56 59	3eqtr3d	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)) \to Z = I (X) \underset{˙}{\cdot} Y$

Metamath Proof Explorer

Theorem slesolinv

Proof