Metamath Proof Explorer

Theorem mavmul0g

Description: The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 mavmul0.t ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
2 oveq12 ⊢ ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ( 𝑋 · 𝑌 ) = ( ∅ · ∅ ) )
3 1 mavmul0 ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ∅ · ∅ ) = ∅ )
4 2 3 sylan9eq ⊢ ( ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ∧ ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ) → ( 𝑋 · 𝑌 ) = ∅ )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 simpr ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
8 0fi ⊢ ∅ ∈ Fin
9 eleq1 ⊢ ( 𝑁 = ∅ → ( 𝑁 ∈ Fin ↔ ∅ ∈ Fin ) )
10 8 9 mpbiri ⊢ ( 𝑁 = ∅ → 𝑁 ∈ Fin )
11 10 adantr ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
12 1 5 6 7 11 11 mvmulfval ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → · = ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) )
13 12 dmeqd ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom · = dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) )
14 0ex ⊢ ∅ ∈ V
15 eleq1 ⊢ ( 𝑁 = ∅ → ( 𝑁 ∈ V ↔ ∅ ∈ V ) )
16 14 15 mpbiri ⊢ ( 𝑁 = ∅ → 𝑁 ∈ V )
17 16 mptexd ⊢ ( 𝑁 = ∅ → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
18 17 adantr ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
19 18 adantr ⊢ ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
20 19 ralrimivva ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ∀ 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∀ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
21 eqid ⊢ ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) )
22 21 dmmpoga ⊢ ( ∀ 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∀ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V → dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
23 20 22 syl ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
24 id ⊢ ( 𝑁 = ∅ → 𝑁 = ∅ )
25 24 24 xpeq12d ⊢ ( 𝑁 = ∅ → ( 𝑁 × 𝑁 ) = ( ∅ × ∅ ) )
26 0xp ⊢ ( ∅ × ∅ ) = ∅
27 25 26 eqtrdi ⊢ ( 𝑁 = ∅ → ( 𝑁 × 𝑁 ) = ∅ )
28 27 oveq2d ⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
29 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
30 map0e ⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
31 29 30 mp1i ⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
32 28 31 eqtrd ⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 1o )
33 32 adantr ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 1o )
34 df1o2 ⊢ 1o = { ∅ }
35 33 34 eqtrdi ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = { ∅ } )
36 oveq2 ⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
37 29 30 mp1i ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
38 37 34 eqtrdi ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = { ∅ } )
39 36 38 sylan9eq ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = { ∅ } )
40 35 39 xpeq12d ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) = ( { ∅ } × { ∅ } ) )
41 13 23 40 3eqtrd ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom · = ( { ∅ } × { ∅ } ) )
42 elsni ⊢ ( 𝑋 ∈ { ∅ } → 𝑋 = ∅ )
43 elsni ⊢ ( 𝑌 ∈ { ∅ } → 𝑌 = ∅ )
44 42 43 anim12i ⊢ ( ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) → ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) )
45 44 con3i ⊢ ( ¬ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ¬ ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) )
46 ndmovg ⊢ ( ( dom · = ( { ∅ } × { ∅ } ) ∧ ¬ ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) ) → ( 𝑋 · 𝑌 ) = ∅ )
47 41 45 46 syl2anr ⊢ ( ( ¬ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ∧ ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ) → ( 𝑋 · 𝑌 ) = ∅ )
48 4 47 pm2.61ian ⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑋 · 𝑌 ) = ∅ )