slesolvec

Description: Every solution of a system of linear equations represented by a matrix and a vector is a vector. (Contributed by AV, 10-Feb-2019) (Revised by AV, 27-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⟩$
Assertion	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)$

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	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
6	5	simpld	$⊢ X \in B \to N \in Fin$
7		simpr	$⊢ (N \neq \emptyset \land N \in Fin) \to N \in Fin$
8		simpl	$⊢ (N \neq \emptyset \land N \in Fin) \to N \neq \emptyset$
9	7 7 8	3jca	$⊢ (N \neq \emptyset \land N \in Fin) \to (N \in Fin \land N \in Fin \land N \neq \emptyset)$
10	9	ex	$⊢ N \neq \emptyset \to (N \in Fin \to (N \in Fin \land N \in Fin \land N \neq \emptyset))$
11	10	adantr	$⊢ (N \neq \emptyset \land R \in Ring) \to (N \in Fin \to (N \in Fin \land N \in Fin \land N \neq \emptyset))$
12	6 11	syl5com	$⊢ X \in B \to ((N \neq \emptyset \land R \in Ring) \to (N \in Fin \land N \in Fin \land N \neq \emptyset))$
13	12	adantr	$⊢ (X \in B \land Y \in V) \to ((N \neq \emptyset \land R \in Ring) \to (N \in Fin \land N \in Fin \land N \neq \emptyset))$
14	13	impcom	$⊢ ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V)) \to (N \in Fin \land N \in Fin \land N \neq \emptyset)$
15		simpr	$⊢ (N \neq \emptyset \land R \in Ring) \to R \in Ring$
16		simpr	$⊢ (X \in B \land Y \in V) \to Y \in V$
17	15 16	anim12i	$⊢ ((N \neq \emptyset \land R \in Ring) \land (X \in B \land Y \in V)) \to (R \in Ring \land Y \in V)$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19		eqid	$⊢ {Base}_{R}^{(N \times N)} = {Base}_{R}^{(N \times N)}$
20	18 19 3 4 3	mavmulsolcl	$⊢ ((N \in Fin \land N \in Fin \land N \neq \emptyset) \land (R \in Ring \land Y \in V)) \to (X \underset{˙}{\cdot} Z = Y \to Z \in V)$
21	14 17 20	syl2anc	$⊢ ((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)$

Metamath Proof Explorer

Theorem slesolvec

Proof