Metamath Proof Explorer

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 ⊢ · ˙ = R maVecMul N N
Assertion mavmul0 ⊢ N = ∅ ∧ R ∈ V → ∅ · ˙ ∅ = ∅

Proof

Step Hyp Ref Expression
1 mavmul0.t ⊢ · ˙ = R maVecMul N N
2 eqid ⊢ N Mat R = N Mat R
3 eqid ⊢ Base R = Base R
4 eqid ⊢ ⋅ R = ⋅ R
5 simpr ⊢ N = ∅ ∧ R ∈ V → R ∈ V
6 0fi ⊢ ∅ ∈ Fin
7 eleq1 ⊢ N = ∅ → N ∈ Fin ↔ ∅ ∈ Fin
8 6 7 mpbiri ⊢ N = ∅ → N ∈ Fin
9 8 adantr ⊢ N = ∅ ∧ R ∈ V → N ∈ Fin
10 0ex ⊢ ∅ ∈ V
11 snidg ⊢ ∅ ∈ V → ∅ ∈ ∅
12 10 11 mp1i ⊢ N = ∅ ∧ R ∈ V → ∅ ∈ ∅
13 oveq1 ⊢ N = ∅ → N Mat R = ∅ Mat R
14 13 adantr ⊢ N = ∅ ∧ R ∈ V → N Mat R = ∅ Mat R
15 14 fveq2d ⊢ N = ∅ ∧ R ∈ V → Base N Mat R = Base ∅ Mat R
16 mat0dimbas0 ⊢ R ∈ V → Base ∅ Mat R = ∅
17 16 adantl ⊢ N = ∅ ∧ R ∈ V → Base ∅ Mat R = ∅
18 15 17 eqtrd ⊢ N = ∅ ∧ R ∈ V → Base N Mat R = ∅
19 12 18 eleqtrrd ⊢ N = ∅ ∧ R ∈ V → ∅ ∈ Base N Mat R
20 eqidd ⊢ N = ∅ → ∅ = ∅
21 el1o ⊢ ∅ ∈ 1 𝑜 ↔ ∅ = ∅
22 20 21 sylibr ⊢ N = ∅ → ∅ ∈ 1 𝑜
23 oveq2 ⊢ N = ∅ → Base R N = Base R ∅
24 fvex ⊢ Base R ∈ V
25 map0e ⊢ Base R ∈ V → Base R ∅ = 1 𝑜
26 24 25 mp1i ⊢ N = ∅ → Base R ∅ = 1 𝑜
27 23 26 eqtrd ⊢ N = ∅ → Base R N = 1 𝑜
28 22 27 eleqtrrd ⊢ N = ∅ → ∅ ∈ Base R N
29 28 adantr ⊢ N = ∅ ∧ R ∈ V → ∅ ∈ Base R N
30 2 1 3 4 5 9 19 29 mavmulval ⊢ N = ∅ ∧ R ∈ V → ∅ · ˙ ∅ = i ∈ N ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j
31 mpteq1 ⊢ N = ∅ → i ∈ N ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j = i ∈ ∅ ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j
32 31 adantr ⊢ N = ∅ ∧ R ∈ V → i ∈ N ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j = i ∈ ∅ ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j
33 mpt0 ⊢ i ∈ ∅ ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j = ∅
34 32 33 eqtrdi ⊢ N = ∅ ∧ R ∈ V → i ∈ N ⟼ ∑ R j ∈ N i ∅ j ⋅ R ∅ ⁡ j = ∅
35 30 34 eqtrd ⊢ N = ∅ ∧ R ∈ V → ∅ · ˙ ∅ = ∅