slesolinvbi

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, 11-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	slesolinvbi	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (X \underset{˙}{\cdot} Z = Y \leftrightarrow 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		simpl1	$⊢ (((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 CRing)$
8		simpl2	$⊢ (((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 B \land Y \in V)$
9		simp3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to D (X) \in Unit (R)$
10	9	anim1i	$⊢ (((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 (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y)$
11	1 2 3 4 5 6	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$
12	7 8 10 11	syl3anc	$⊢ (((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$
13		oveq2	$⊢ Z = I (X) \underset{˙}{\cdot} Y \to X \underset{˙}{\cdot} Z = X \underset{˙}{\cdot} (I (X) \underset{˙}{\cdot} Y)$
14		simpr	$⊢ (N \neq \emptyset \land R \in CRing) \to R \in CRing$
15	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
16	15	simpld	$⊢ X \in B \to N \in Fin$
17	16	adantr	$⊢ (X \in B \land Y \in V) \to N \in Fin$
18	14 17	anim12ci	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (N \in Fin \land R \in CRing)$
19	18	3adant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (N \in Fin \land R \in CRing)$
20		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
21	1 20	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
22	19 21	syl	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
23	22	oveqd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X (R maMul ⟨N, N, N⟩) I (X) = X \cdot_{A} I (X)$
24		crngring	$⊢ R \in CRing \to R \in Ring$
25	24	adantl	$⊢ (N \neq \emptyset \land R \in CRing) \to R \in Ring$
26	25 17	anim12ci	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (N \in Fin \land R \in Ring)$
27	26	3adant3	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (N \in Fin \land R \in Ring)$
28	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
29	27 28	syl	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to A \in Ring$
30		eqid	$⊢ Unit (A) = Unit (A)$
31		eqid	$⊢ Unit (R) = Unit (R)$
32	1 5 2 30 31	matunit	$⊢ (R \in CRing \land X \in B) \to (X \in Unit (A) \leftrightarrow D (X) \in Unit (R))$
33	32	ad2ant2lr	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V)) \to (X \in Unit (A) \leftrightarrow D (X) \in Unit (R))$
34	33	biimp3ar	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X \in Unit (A)$
35		eqid	$⊢ \cdot_{A} = \cdot_{A}$
36		eqid	$⊢ 1_{A} = 1_{A}$
37	30 6 35 36	unitrinv	$⊢ (A \in Ring \land X \in Unit (A)) \to X \cdot_{A} I (X) = 1_{A}$
38	29 34 37	syl2anc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X \cdot_{A} I (X) = 1_{A}$
39	23 38	eqtrd	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X (R maMul ⟨N, N, N⟩) I (X) = 1_{A}$
40	39	oveq1d	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (X (R maMul ⟨N, N, N⟩) I (X)) \underset{˙}{\cdot} Y = 1_{A} \underset{˙}{\cdot} Y$
41		eqid	$⊢ {Base}_{R} = {Base}_{R}$
42	25	3ad2ant1	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to R \in Ring$
43	17	3ad2ant2	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to N \in Fin$
44	3	eleq2i	$⊢ Y \in V \leftrightarrow Y \in ({Base}_{R}^{N})$
45	44	biimpi	$⊢ Y \in V \to Y \in ({Base}_{R}^{N})$
46	45	adantl	$⊢ (X \in B \land Y \in V) \to Y \in ({Base}_{R}^{N})$
47	46	3ad2ant2	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to Y \in ({Base}_{R}^{N})$
48	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
49	48	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
50	49	adantr	$⊢ (X \in B \land Y \in V) \to X \in {Base}_{A}$
51	50	3ad2ant2	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X \in {Base}_{A}$
52		eqid	$⊢ {Base}_{A} = {Base}_{A}$
53	30 6 52	ringinvcl	$⊢ (A \in Ring \land X \in Unit (A)) \to I (X) \in {Base}_{A}$
54	29 34 53	syl2anc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to I (X) \in {Base}_{A}$
55	1 41 4 42 43 47 20 51 54	mavmulass	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (X (R maMul ⟨N, N, N⟩) I (X)) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} (I (X) \underset{˙}{\cdot} Y)$
56	1 41 4 42 43 47	1mavmul	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to 1_{A} \underset{˙}{\cdot} Y = Y$
57	40 55 56	3eqtr3d	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to X \underset{˙}{\cdot} (I (X) \underset{˙}{\cdot} Y) = Y$
58	13 57	sylan9eqr	$⊢ (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land Z = I (X) \underset{˙}{\cdot} Y) \to X \underset{˙}{\cdot} Z = Y$
59	12 58	impbida	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (X \underset{˙}{\cdot} Z = Y \leftrightarrow Z = I (X) \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem slesolinvbi

Proof