mavmulsolcl

Description: Every solution of the equation A * X = Y for a matrix A and a vector B is a vector. (Contributed by AV, 27-Feb-2019)

	Ref	Expression
Hypotheses	mavmuldm.b	$⊢ B = {Base}_{R}$
	mavmuldm.c	$⊢ C = B^{(M \times N)}$
	mavmuldm.d	$⊢ D = B^{N}$
	mavmuldm.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨M, N⟩$
	mavmulsolcl.e	$⊢ E = B^{M}$
Assertion	mavmulsolcl	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (A \underset{˙}{\cdot} X = Y \to X \in D)$

Proof

Step	Hyp	Ref	Expression
1		mavmuldm.b	$⊢ B = {Base}_{R}$
2		mavmuldm.c	$⊢ C = B^{(M \times N)}$
3		mavmuldm.d	$⊢ D = B^{N}$
4		mavmuldm.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨M, N⟩$
5		mavmulsolcl.e	$⊢ E = B^{M}$
6		2a1	$⊢ X \in D \to (((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (A \underset{˙}{\cdot} X = Y \to X \in D))$
7		simpl	$⊢ (R \in V \land Y \in E) \to R \in V$
8	7	adantl	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to R \in V$
9		simpl1	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to M \in Fin$
10		simpl2	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to N \in Fin$
11	8 9 10	3jca	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (R \in V \land M \in Fin \land N \in Fin)$
12	11	adantl	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to (R \in V \land M \in Fin \land N \in Fin)$
13	1 2 3 4	mavmuldm	$⊢ (R \in V \land M \in Fin \land N \in Fin) \to dom \underset{˙}{\cdot} = C \times D$
14	12 13	syl	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to dom \underset{˙}{\cdot} = C \times D$
15		simpl	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to \neg X \in D$
16	15	intnand	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to \neg (A \in C \land X \in D)$
17		ndmovg	$⊢ (dom \underset{˙}{\cdot} = C \times D \land \neg (A \in C \land X \in D)) \to A \underset{˙}{\cdot} X = \emptyset$
18	14 16 17	syl2anc	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to A \underset{˙}{\cdot} X = \emptyset$
19		eqeq1	$⊢ A \underset{˙}{\cdot} X = \emptyset \to (A \underset{˙}{\cdot} X = Y \leftrightarrow \emptyset = Y)$
20		elmapi	$⊢ Y \in (B^{M}) \to Y : M ⟶ B$
21		f0dom0	$⊢ Y : M ⟶ B \to (M = \emptyset \leftrightarrow Y = \emptyset)$
22	21	biimprd	$⊢ Y : M ⟶ B \to (Y = \emptyset \to M = \emptyset)$
23	22	necon3d	$⊢ Y : M ⟶ B \to (M \neq \emptyset \to Y \neq \emptyset)$
24	23	com12	$⊢ M \neq \emptyset \to (Y : M ⟶ B \to Y \neq \emptyset)$
25	24	3ad2ant3	$⊢ (M \in Fin \land N \in Fin \land M \neq \emptyset) \to (Y : M ⟶ B \to Y \neq \emptyset)$
26	25	com12	$⊢ Y : M ⟶ B \to ((M \in Fin \land N \in Fin \land M \neq \emptyset) \to Y \neq \emptyset)$
27	26	a1d	$⊢ Y : M ⟶ B \to (R \in V \to ((M \in Fin \land N \in Fin \land M \neq \emptyset) \to Y \neq \emptyset))$
28	20 27	syl	$⊢ Y \in (B^{M}) \to (R \in V \to ((M \in Fin \land N \in Fin \land M \neq \emptyset) \to Y \neq \emptyset))$
29	28 5	eleq2s	$⊢ Y \in E \to (R \in V \to ((M \in Fin \land N \in Fin \land M \neq \emptyset) \to Y \neq \emptyset))$
30	29	impcom	$⊢ (R \in V \land Y \in E) \to ((M \in Fin \land N \in Fin \land M \neq \emptyset) \to Y \neq \emptyset)$
31	30	impcom	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to Y \neq \emptyset$
32		eqneqall	$⊢ Y = \emptyset \to (Y \neq \emptyset \to X \in D)$
33	31 32	syl5com	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (Y = \emptyset \to X \in D)$
34	33	adantl	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to (Y = \emptyset \to X \in D)$
35	34	com12	$⊢ Y = \emptyset \to ((\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to X \in D)$
36	35	eqcoms	$⊢ \emptyset = Y \to ((\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to X \in D)$
37	19 36	syl6bi	$⊢ A \underset{˙}{\cdot} X = \emptyset \to (A \underset{˙}{\cdot} X = Y \to ((\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to X \in D))$
38	37	com23	$⊢ A \underset{˙}{\cdot} X = \emptyset \to ((\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to (A \underset{˙}{\cdot} X = Y \to X \in D))$
39	18 38	mpcom	$⊢ (\neg X \in D \land ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E))) \to (A \underset{˙}{\cdot} X = Y \to X \in D)$
40	39	ex	$⊢ \neg X \in D \to (((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (A \underset{˙}{\cdot} X = Y \to X \in D))$
41	6 40	pm2.61i	$⊢ ((M \in Fin \land N \in Fin \land M \neq \emptyset) \land (R \in V \land Y \in E)) \to (A \underset{˙}{\cdot} X = Y \to X \in D)$

Metamath Proof Explorer

Theorem mavmulsolcl

Proof