mavmul0g

Description: The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019)

		Ref	Expression
	Hypothesis	mavmul0.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	Assertion	mavmul0g	$⊢ (N = \emptyset \land R \in V) \to X \underset{˙}{\cdot} Y = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		mavmul0.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
2		oveq12	$⊢ (X = \emptyset \land Y = \emptyset) \to X \underset{˙}{\cdot} Y = \emptyset \underset{˙}{\cdot} \emptyset$
3	1	mavmul0	$⊢ (N = \emptyset \land R \in V) \to \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$
4	2 3	sylan9eq	$⊢ ((X = \emptyset \land Y = \emptyset) \land (N = \emptyset \land R \in V)) \to X \underset{˙}{\cdot} Y = \emptyset$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		simpr	$⊢ (N = \emptyset \land R \in V) \to R \in V$
8		0fi	$⊢ \emptyset \in Fin$
9		eleq1	$⊢ N = \emptyset \to (N \in Fin \leftrightarrow \emptyset \in Fin)$
10	8 9	mpbiri	$⊢ N = \emptyset \to N \in Fin$
11	10	adantr	$⊢ (N = \emptyset \land R \in V) \to N \in Fin$
12	1 5 6 7 11 11	mvmulfval	$⊢ (N = \emptyset \land R \in V) \to \underset{˙}{\cdot} = (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))))$
13	12	dmeqd	$⊢ (N = \emptyset \land R \in V) \to dom \underset{˙}{\cdot} = dom (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))))$
14		0ex	$⊢ \emptyset \in V$
15		eleq1	$⊢ N = \emptyset \to (N \in V \leftrightarrow \emptyset \in V)$
16	14 15	mpbiri	$⊢ N = \emptyset \to N \in V$
17	16	mptexd	$⊢ N = \emptyset \to (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))) \in V$
18	17	adantr	$⊢ (N = \emptyset \land R \in V) \to (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))) \in V$
19	18	adantr	$⊢ ((N = \emptyset \land R \in V) \land (i \in ({Base}_{R}^{(N \times N)}) \land j \in ({Base}_{R}^{N}))) \to (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))) \in V$
20	19	ralrimivva	$⊢ (N = \emptyset \land R \in V) \to \forall i \in ({Base}_{R}^{(N \times N)}) \forall j \in ({Base}_{R}^{N}) (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))) \in V$
21		eqid	$⊢ (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l)))) = (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))))$
22	21	dmmpoga	$⊢ \forall i \in ({Base}_{R}^{(N \times N)}) \forall j \in ({Base}_{R}^{N}) (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l))) \in V \to dom (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l)))) = ({Base}_{R}^{(N \times N)}) \times ({Base}_{R}^{N})$
23	20 22	syl	$⊢ (N = \emptyset \land R \in V) \to dom (i \in ({Base}_{R}^{(N \times N)}), j \in ({Base}_{R}^{N}) ⟼ (k \in N ⟼ \underset{l \in N}{\sum_{R}} ((k i l) \cdot_{R} j (l)))) = ({Base}_{R}^{(N \times N)}) \times ({Base}_{R}^{N})$
24		id	$⊢ N = \emptyset \to N = \emptyset$
25	24 24	xpeq12d	$⊢ N = \emptyset \to N \times N = \emptyset \times \emptyset$
26		0xp	$⊢ \emptyset \times \emptyset = \emptyset$
27	25 26	eqtrdi	$⊢ N = \emptyset \to N \times N = \emptyset$
28	27	oveq2d	$⊢ N = \emptyset \to {Base}_{R}^{(N \times N)} = {Base}_{R}^{\emptyset}$
29		fvex	$⊢ {Base}_{R} \in V$
30		map0e	$⊢ {Base}_{R} \in V \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
31	29 30	mp1i	$⊢ N = \emptyset \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
32	28 31	eqtrd	$⊢ N = \emptyset \to {Base}_{R}^{(N \times N)} = 1_{𝑜}$
33	32	adantr	$⊢ (N = \emptyset \land R \in V) \to {Base}_{R}^{(N \times N)} = 1_{𝑜}$
34		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
35	33 34	eqtrdi	$⊢ (N = \emptyset \land R \in V) \to {Base}_{R}^{(N \times N)} = \{\emptyset\}$
36		oveq2	$⊢ N = \emptyset \to {Base}_{R}^{N} = {Base}_{R}^{\emptyset}$
37	29 30	mp1i	$⊢ R \in V \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
38	37 34	eqtrdi	$⊢ R \in V \to {Base}_{R}^{\emptyset} = \{\emptyset\}$
39	36 38	sylan9eq	$⊢ (N = \emptyset \land R \in V) \to {Base}_{R}^{N} = \{\emptyset\}$
40	35 39	xpeq12d	$⊢ (N = \emptyset \land R \in V) \to ({Base}_{R}^{(N \times N)}) \times ({Base}_{R}^{N}) = \{\emptyset\} \times \{\emptyset\}$
41	13 23 40	3eqtrd	$⊢ (N = \emptyset \land R \in V) \to dom \underset{˙}{\cdot} = \{\emptyset\} \times \{\emptyset\}$
42		elsni	$⊢ X \in \{\emptyset\} \to X = \emptyset$
43		elsni	$⊢ Y \in \{\emptyset\} \to Y = \emptyset$
44	42 43	anim12i	$⊢ (X \in \{\emptyset\} \land Y \in \{\emptyset\}) \to (X = \emptyset \land Y = \emptyset)$
45	44	con3i	$⊢ \neg (X = \emptyset \land Y = \emptyset) \to \neg (X \in \{\emptyset\} \land Y \in \{\emptyset\})$
46		ndmovg	$⊢ (dom \underset{˙}{\cdot} = \{\emptyset\} \times \{\emptyset\} \land \neg (X \in \{\emptyset\} \land Y \in \{\emptyset\})) \to X \underset{˙}{\cdot} Y = \emptyset$
47	41 45 46	syl2anr	$⊢ (\neg (X = \emptyset \land Y = \emptyset) \land (N = \emptyset \land R \in V)) \to X \underset{˙}{\cdot} Y = \emptyset$
48	4 47	pm2.61ian	$⊢ (N = \emptyset \land R \in V) \to X \underset{˙}{\cdot} Y = \emptyset$

Metamath Proof Explorer

Theorem mavmul0g

Proof