Theorem mavmul0

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

	Ref	Expression
Hypothesis	mavmul0.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
Assertion	mavmul0	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ∅ · ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mavmul0.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
2		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5		simpr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
6		0fi	⊢ ∅ ∈ Fin
7		eleq1	⊢ ( 𝑁 = ∅ → ( 𝑁 ∈ Fin ↔ ∅ ∈ Fin ) )
8	6 7	mpbiri	⊢ ( 𝑁 = ∅ → 𝑁 ∈ Fin )
9	8	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
10		0ex	⊢ ∅ ∈ V
11		snidg	⊢ ( ∅ ∈ V → ∅ ∈ { ∅ } )
12	10 11	mp1i	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ∅ ∈ { ∅ } )
13		oveq1	⊢ ( 𝑁 = ∅ → ( 𝑁 Mat 𝑅 ) = ( ∅ Mat 𝑅 ) )
14	13	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 Mat 𝑅 ) = ( ∅ Mat 𝑅 ) )
15	14	fveq2d	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
16		mat0dimbas0	⊢ ( 𝑅 ∈ 𝑉 → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
17	16	adantl	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
18	15 17	eqtrd	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = { ∅ } )
19	12 18	eleqtrrd	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ∅ ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
20		eqidd	⊢ ( 𝑁 = ∅ → ∅ = ∅ )
21		el1o	⊢ ( ∅ ∈ 1o ↔ ∅ = ∅ )
22	20 21	sylibr	⊢ ( 𝑁 = ∅ → ∅ ∈ 1o )
23		oveq2	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
24		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
25		map0e	⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
26	24 25	mp1i	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
27	23 26	eqtrd	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = 1o )
28	22 27	eleqtrrd	⊢ ( 𝑁 = ∅ → ∅ ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
29	28	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ∅ ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
30	2 1 3 4 5 9 19 29	mavmulval	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ∅ · ∅ ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) )
31		mpteq1	⊢ ( 𝑁 = ∅ → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) )
32	31	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) )
33		mpt0	⊢ ( 𝑖 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) = ∅
34	32 33	eqtrdi	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ∅ 𝑗 ) ( .r ‘ 𝑅 ) ( ∅ ‘ 𝑗 ) ) ) ) ) = ∅ )
35	30 34	eqtrd	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ∅ · ∅ ) = ∅ )