mavmul0

Description: Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mavmul0.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
2		eqid	$⊢ N Mat R = N Mat R$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		simpr	$⊢ (N = \emptyset \land R \in V) \to R \in V$
6		0fin	$⊢ \emptyset \in Fin$
7		eleq1	$⊢ N = \emptyset \to (N \in Fin \leftrightarrow \emptyset \in Fin)$
8	6 7	mpbiri	$⊢ N = \emptyset \to N \in Fin$
9	8	adantr	$⊢ (N = \emptyset \land R \in V) \to N \in Fin$
10		0ex	$⊢ \emptyset \in V$
11		snidg	$⊢ \emptyset \in V \to \emptyset \in \{\emptyset\}$
12	10 11	mp1i	$⊢ (N = \emptyset \land R \in V) \to \emptyset \in \{\emptyset\}$
13		oveq1	$⊢ N = \emptyset \to N Mat R = \emptyset Mat R$
14	13	adantr	$⊢ (N = \emptyset \land R \in V) \to N Mat R = \emptyset Mat R$
15	14	fveq2d	$⊢ (N = \emptyset \land R \in V) \to {Base}_{(N Mat R)} = {Base}_{(\emptyset Mat R)}$
16		mat0dimbas0	$⊢ R \in V \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
17	16	adantl	$⊢ (N = \emptyset \land R \in V) \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
18	15 17	eqtrd	$⊢ (N = \emptyset \land R \in V) \to {Base}_{(N Mat R)} = \{\emptyset\}$
19	12 18	eleqtrrd	$⊢ (N = \emptyset \land R \in V) \to \emptyset \in {Base}_{(N Mat R)}$
20		eqidd	$⊢ N = \emptyset \to \emptyset = \emptyset$
21		el1o	$⊢ \emptyset \in 1_{𝑜} \leftrightarrow \emptyset = \emptyset$
22	20 21	sylibr	$⊢ N = \emptyset \to \emptyset \in 1_{𝑜}$
23		oveq2	$⊢ N = \emptyset \to {Base}_{R}^{N} = {Base}_{R}^{\emptyset}$
24		fvex	$⊢ {Base}_{R} \in V$
25		map0e	$⊢ {Base}_{R} \in V \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
26	24 25	mp1i	$⊢ N = \emptyset \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
27	23 26	eqtrd	$⊢ N = \emptyset \to {Base}_{R}^{N} = 1_{𝑜}$
28	22 27	eleqtrrd	$⊢ N = \emptyset \to \emptyset \in ({Base}_{R}^{N})$
29	28	adantr	$⊢ (N = \emptyset \land R \in V) \to \emptyset \in ({Base}_{R}^{N})$
30	2 1 3 4 5 9 19 29	mavmulval	$⊢ (N = \emptyset \land R \in V) \to \emptyset \underset{˙}{\cdot} \emptyset = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j)))$
31		mpteq1	$⊢ N = \emptyset \to (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j))) = (i \in \emptyset ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j)))$
32	31	adantr	$⊢ (N = \emptyset \land R \in V) \to (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j))) = (i \in \emptyset ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j)))$
33		mpt0	$⊢ (i \in \emptyset ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j))) = \emptyset$
34	32 33	eqtrdi	$⊢ (N = \emptyset \land R \in V) \to (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i \emptyset j) \cdot_{R} \emptyset (j))) = \emptyset$
35	30 34	eqtrd	$⊢ (N = \emptyset \land R \in V) \to \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$

Metamath Proof Explorer

Theorem mavmul0

Proof