mamufacex

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

	Ref	Expression
Hypotheses	mamudm.e	$⊢ E = R freeLMod (M \times N)$
	mamudm.b	$⊢ B = {Base}_{E}$
	mamudm.f	$⊢ F = R freeLMod (N \times P)$
	mamudm.c	$⊢ C = {Base}_{F}$
	mamudm.m	$⊢ \underset{˙}{\times} = R maMul ⟨M, N, P⟩$
	mamufacex.g	$⊢ G = R freeLMod (M \times P)$
	mamufacex.d	$⊢ D = {Base}_{G}$
Assertion	mamufacex	$⊢ ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (X \underset{˙}{\times} Z = Y \to Z \in C)$

Proof

Step	Hyp	Ref	Expression
1		mamudm.e	$⊢ E = R freeLMod (M \times N)$
2		mamudm.b	$⊢ B = {Base}_{E}$
3		mamudm.f	$⊢ F = R freeLMod (N \times P)$
4		mamudm.c	$⊢ C = {Base}_{F}$
5		mamudm.m	$⊢ \underset{˙}{\times} = R maMul ⟨M, N, P⟩$
6		mamufacex.g	$⊢ G = R freeLMod (M \times P)$
7		mamufacex.d	$⊢ D = {Base}_{G}$
8		2a1	$⊢ Z \in C \to (((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (X \underset{˙}{\times} Z = Y \to Z \in C))$
9	1 2 3 4 5	mamudm	$⊢ (R \in V \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = B \times C$
10	9	adantlr	$⊢ ((R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = B \times C$
11	10	3adant1	$⊢ ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to dom \underset{˙}{\times} = B \times C$
12		simpl	$⊢ (\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to \neg Z \in C$
13	12	intnand	$⊢ (\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to \neg (X \in B \land Z \in C)$
14		ndmovg	$⊢ (dom \underset{˙}{\times} = B \times C \land \neg (X \in B \land Z \in C)) \to X \underset{˙}{\times} Z = \emptyset$
15	11 13 14	syl2an2	$⊢ (\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to X \underset{˙}{\times} Z = \emptyset$
16		eqeq1	$⊢ X \underset{˙}{\times} Z = \emptyset \to (X \underset{˙}{\times} Z = Y \leftrightarrow \emptyset = Y)$
17		xpfi	$⊢ (M \in Fin \land P \in Fin) \to M \times P \in Fin$
18	17	3adant2	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to M \times P \in Fin$
19		xpnz	$⊢ (M \neq \emptyset \land P \neq \emptyset) \leftrightarrow M \times P \neq \emptyset$
20	19	biimpi	$⊢ (M \neq \emptyset \land P \neq \emptyset) \to M \times P \neq \emptyset$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22	6 21 7	elfrlmbasn0	$⊢ (M \times P \in Fin \land M \times P \neq \emptyset) \to (Y \in D \to Y \neq \emptyset)$
23	18 20 22	syl2an	$⊢ ((M \in Fin \land N \in Fin \land P \in Fin) \land (M \neq \emptyset \land P \neq \emptyset)) \to (Y \in D \to Y \neq \emptyset)$
24	23	ex	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to ((M \neq \emptyset \land P \neq \emptyset) \to (Y \in D \to Y \neq \emptyset))$
25	24	com13	$⊢ Y \in D \to ((M \neq \emptyset \land P \neq \emptyset) \to ((M \in Fin \land N \in Fin \land P \in Fin) \to Y \neq \emptyset))$
26	25	adantl	$⊢ (R \in V \land Y \in D) \to ((M \neq \emptyset \land P \neq \emptyset) \to ((M \in Fin \land N \in Fin \land P \in Fin) \to Y \neq \emptyset))$
27	26	3imp21	$⊢ ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to Y \neq \emptyset$
28		eqneqall	$⊢ Y = \emptyset \to (Y \neq \emptyset \to Z \in C)$
29	27 28	syl5com	$⊢ ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (Y = \emptyset \to Z \in C)$
30	29	adantl	$⊢ (\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to (Y = \emptyset \to Z \in C)$
31	30	com12	$⊢ Y = \emptyset \to ((\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to Z \in C)$
32	31	eqcoms	$⊢ \emptyset = Y \to ((\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to Z \in C)$
33	16 32	syl6bi	$⊢ X \underset{˙}{\times} Z = \emptyset \to (X \underset{˙}{\times} Z = Y \to ((\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to Z \in C))$
34	33	com23	$⊢ X \underset{˙}{\times} Z = \emptyset \to ((\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to (X \underset{˙}{\times} Z = Y \to Z \in C))$
35	15 34	mpcom	$⊢ (\neg Z \in C \land ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin))) \to (X \underset{˙}{\times} Z = Y \to Z \in C)$
36	35	ex	$⊢ \neg Z \in C \to (((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (X \underset{˙}{\times} Z = Y \to Z \in C))$
37	8 36	pm2.61i	$⊢ ((M \neq \emptyset \land P \neq \emptyset) \land (R \in V \land Y \in D) \land (M \in Fin \land N \in Fin \land P \in Fin)) \to (X \underset{˙}{\times} Z = Y \to Z \in C)$

Metamath Proof Explorer

Theorem mamufacex

Proof