slesolex

Description: Every system of linear equations represented by a matrix with a unit as determinant has a solution. (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$
Assertion	slesolex	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \exists z \in V X \underset{˙}{\cdot} z = 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		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ \cdot_{R} = \cdot_{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)) \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)) \to N \in Fin$
15	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)$
16	15	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)$
17	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
18	16 17	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$
19		eqid	$⊢ Unit (A) = Unit (A)$
20		eqid	$⊢ Unit (R) = Unit (R)$
21	1 5 2 19 20	matunit	$⊢ (R \in CRing \land X \in B) \to (X \in Unit (A) \leftrightarrow D (X) \in Unit (R))$
22	21	bicomd	$⊢ (R \in CRing \land X \in B) \to (D (X) \in Unit (R) \leftrightarrow X \in Unit (A))$
23	22	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))$
24	23	biimp3a	$⊢ ((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)$
25		eqid	$⊢ {inv}_{r} (A) = {inv}_{r} (A)$
26		eqid	$⊢ {Base}_{A} = {Base}_{A}$
27	19 25 26	ringinvcl	$⊢ (A \in Ring \land X \in Unit (A)) \to {inv}_{r} (A) (X) \in {Base}_{A}$
28	18 24 27	syl2anc	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to {inv}_{r} (A) (X) \in {Base}_{A}$
29	3	eleq2i	$⊢ Y \in V \leftrightarrow Y \in ({Base}_{R}^{N})$
30	29	biimpi	$⊢ Y \in V \to Y \in ({Base}_{R}^{N})$
31	30	adantl	$⊢ (X \in B \land Y \in V) \to Y \in ({Base}_{R}^{N})$
32	31	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})$
33	1 4 6 7 10 14 28 32	mavmulcl	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to {inv}_{r} (A) (X) \underset{˙}{\cdot} Y \in ({Base}_{R}^{N})$
34	33 3	eleqtrrdi	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to {inv}_{r} (A) (X) \underset{˙}{\cdot} Y \in V$
35	1 2 3 4 5 25	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 = {inv}_{r} (A) (X) \underset{˙}{\cdot} Y)$
36	35	adantr	$⊢ (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land ((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 = {inv}_{r} (A) (X) \underset{˙}{\cdot} Y)$
37	36	biimprd	$⊢ (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R))) \to (z = {inv}_{r} (A) (X) \underset{˙}{\cdot} Y \to X \underset{˙}{\cdot} z = Y)$
38	37	impancom	$⊢ (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land z = {inv}_{r} (A) (X) \underset{˙}{\cdot} Y) \to (((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)$
39	34 38	rspcimedv	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \exists z \in V X \underset{˙}{\cdot} z = Y)$
40	39	pm2.43i	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \exists z \in V X \underset{˙}{\cdot} z = Y$

Metamath Proof Explorer

Theorem slesolex

Proof