Step | Hyp | Ref
| Expression |
1 | | oveq12 6931 |
. . 3
⊢ ((𝑋 = ∅ ∧ 𝑌 = ∅) → (𝑋 · 𝑌) = (∅ ·
∅)) |
2 | | mavmul0.t |
. . . 4
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
3 | 2 | mavmul0 20763 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (∅ · ∅) =
∅) |
4 | 1, 3 | sylan9eq 2834 |
. 2
⊢ (((𝑋 = ∅ ∧ 𝑌 = ∅) ∧ (𝑁 = ∅ ∧ 𝑅 ∈ 𝑉)) → (𝑋 · 𝑌) = ∅) |
5 | | eqid 2778 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2778 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
7 | | simpr 479 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) |
8 | | 0fin 8476 |
. . . . . . . 8
⊢ ∅
∈ Fin |
9 | | eleq1 2847 |
. . . . . . . 8
⊢ (𝑁 = ∅ → (𝑁 ∈ Fin ↔ ∅
∈ Fin)) |
10 | 8, 9 | mpbiri 250 |
. . . . . . 7
⊢ (𝑁 = ∅ → 𝑁 ∈ Fin) |
11 | 10 | adantr 474 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
12 | 2, 5, 6, 7, 11, 11 | mvmulfval 20753 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → · = (𝑖 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))))) |
13 | 12 | dmeqd 5571 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → dom · = dom (𝑖 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))))) |
14 | | 0ex 5026 |
. . . . . . . . . 10
⊢ ∅
∈ V |
15 | | eleq1 2847 |
. . . . . . . . . 10
⊢ (𝑁 = ∅ → (𝑁 ∈ V ↔ ∅ ∈
V)) |
16 | 14, 15 | mpbiri 250 |
. . . . . . . . 9
⊢ (𝑁 = ∅ → 𝑁 ∈ V) |
17 | | mptexg 6756 |
. . . . . . . . 9
⊢ (𝑁 ∈ V → (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑁 = ∅ → (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V) |
19 | 18 | adantr 474 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V) |
20 | 19 | adantr 474 |
. . . . . 6
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) ∧ (𝑖 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ∧ 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁))) → (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V) |
21 | 20 | ralrimivva 3153 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → ∀𝑖 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))∀𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁)(𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V) |
22 | | eqid 2778 |
. . . . . 6
⊢ (𝑖 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙)))))) = (𝑖 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙)))))) |
23 | 22 | dmmpt2ga 7522 |
. . . . 5
⊢
(∀𝑖 ∈
((Base‘𝑅)
↑𝑚 (𝑁 × 𝑁))∀𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁)(𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙))))) ∈ V → dom (𝑖 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙)))))) = (((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) × ((Base‘𝑅) ↑𝑚 𝑁))) |
24 | 21, 23 | syl 17 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → dom (𝑖 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)), 𝑗 ∈ ((Base‘𝑅) ↑𝑚 𝑁) ↦ (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑘𝑖𝑙)(.r‘𝑅)(𝑗‘𝑙)))))) = (((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) × ((Base‘𝑅) ↑𝑚 𝑁))) |
25 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑁 = ∅ → 𝑁 = ∅) |
26 | 25, 25 | xpeq12d 5386 |
. . . . . . . . . 10
⊢ (𝑁 = ∅ → (𝑁 × 𝑁) = (∅ ×
∅)) |
27 | | 0xp 5447 |
. . . . . . . . . 10
⊢ (∅
× ∅) = ∅ |
28 | 26, 27 | syl6eq 2830 |
. . . . . . . . 9
⊢ (𝑁 = ∅ → (𝑁 × 𝑁) = ∅) |
29 | 28 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑𝑚 (𝑁 × 𝑁)) = ((Base‘𝑅) ↑𝑚
∅)) |
30 | | fvex 6459 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
31 | | map0e 8179 |
. . . . . . . . 9
⊢
((Base‘𝑅)
∈ V → ((Base‘𝑅) ↑𝑚 ∅) =
1o) |
32 | 30, 31 | mp1i 13 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑𝑚 ∅) = 1o) |
33 | 29, 32 | eqtrd 2814 |
. . . . . . 7
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑𝑚 (𝑁 × 𝑁)) = 1o) |
34 | 33 | adantr 474 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) = 1o) |
35 | | df1o2 7856 |
. . . . . 6
⊢
1o = {∅} |
36 | 34, 35 | syl6eq 2830 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) = {∅}) |
37 | | oveq2 6930 |
. . . . . 6
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑𝑚 𝑁) = ((Base‘𝑅) ↑𝑚
∅)) |
38 | 30, 31 | mp1i 13 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ((Base‘𝑅) ↑𝑚 ∅) =
1o) |
39 | 38, 35 | syl6eq 2830 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → ((Base‘𝑅) ↑𝑚 ∅) =
{∅}) |
40 | 37, 39 | sylan9eq 2834 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → ((Base‘𝑅) ↑𝑚 𝑁) = {∅}) |
41 | 36, 40 | xpeq12d 5386 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) × ((Base‘𝑅) ↑𝑚 𝑁)) = ({∅} ×
{∅})) |
42 | 13, 24, 41 | 3eqtrd 2818 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → dom · = ({∅}
× {∅})) |
43 | | elsni 4415 |
. . . . 5
⊢ (𝑋 ∈ {∅} → 𝑋 = ∅) |
44 | | elsni 4415 |
. . . . 5
⊢ (𝑌 ∈ {∅} → 𝑌 = ∅) |
45 | 43, 44 | anim12i 606 |
. . . 4
⊢ ((𝑋 ∈ {∅} ∧ 𝑌 ∈ {∅}) → (𝑋 = ∅ ∧ 𝑌 = ∅)) |
46 | 45 | con3i 152 |
. . 3
⊢ (¬
(𝑋 = ∅ ∧ 𝑌 = ∅) → ¬ (𝑋 ∈ {∅} ∧ 𝑌 ∈
{∅})) |
47 | | ndmovg 7094 |
. . 3
⊢ ((dom
·
= ({∅} × {∅}) ∧ ¬ (𝑋 ∈ {∅} ∧ 𝑌 ∈ {∅})) → (𝑋 · 𝑌) = ∅) |
48 | 42, 46, 47 | syl2anr 590 |
. 2
⊢ ((¬
(𝑋 = ∅ ∧ 𝑌 = ∅) ∧ (𝑁 = ∅ ∧ 𝑅 ∈ 𝑉)) → (𝑋 · 𝑌) = ∅) |
49 | 4, 48 | pm2.61ian 802 |
1
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (𝑋 · 𝑌) = ∅) |