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 · = ( 𝑅 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 0fin ∅ ∈ 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 ( ( 𝑁 = ∅ ∧ 𝑅𝑉 ) → ( ∅ · ∅ ) = ∅ )