This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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