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