Step | Hyp | Ref
| Expression |
1 | | ral0 4440 |
. . . . . 6
⊢
∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)) |
2 | 1 | 2a1i 12 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → ((∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀))
→ ∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)))) |
3 | | 0ex 5226 |
. . . . . 6
⊢ ∅
∈ V |
4 | | breq1 5073 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ↔ ∅ finSupp
(0g‘(Scalar‘𝑀)))) |
5 | | oveq1 7262 |
. . . . . . . . . 10
⊢ (𝑓 = ∅ → (𝑓( linC ‘𝑀)∅) = (∅( linC ‘𝑀)∅)) |
6 | 5 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → ((𝑓( linC ‘𝑀)∅) = (0g‘𝑀) ↔ (∅( linC
‘𝑀)∅) =
(0g‘𝑀))) |
7 | 4, 6 | anbi12d 630 |
. . . . . . . 8
⊢ (𝑓 = ∅ → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) ↔ (∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀)))) |
8 | | fveq1 6755 |
. . . . . . . . . 10
⊢ (𝑓 = ∅ → (𝑓‘𝑥) = (∅‘𝑥)) |
9 | 8 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → ((𝑓‘𝑥) = (0g‘(Scalar‘𝑀)) ↔ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)))) |
10 | 9 | ralbidv 3120 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)) ↔ ∀𝑥 ∈ ∅
(∅‘𝑥) =
(0g‘(Scalar‘𝑀)))) |
11 | 7, 10 | imbi12d 344 |
. . . . . . 7
⊢ (𝑓 = ∅ → (((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))) ↔ ((∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀))
→ ∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀))))) |
12 | 11 | ralsng 4606 |
. . . . . 6
⊢ (∅
∈ V → (∀𝑓
∈ {∅} ((𝑓
finSupp (0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))) ↔ ((∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀))
→ ∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀))))) |
13 | 3, 12 | mp1i 13 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → (∀𝑓 ∈ {∅} ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))) ↔ ((∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀))
→ ∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀))))) |
14 | 2, 13 | mpbird 256 |
. . . 4
⊢ (𝑀 ∈ 𝑉 → ∀𝑓 ∈ {∅} ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))) |
15 | | fvex 6769 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
16 | | map0e 8628 |
. . . . . . 7
⊢
((Base‘(Scalar‘𝑀)) ∈ V →
((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) |
17 | 15, 16 | mp1i 13 |
. . . . . 6
⊢ (𝑀 ∈ 𝑉 → ((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) |
18 | | df1o2 8279 |
. . . . . 6
⊢
1o = {∅} |
19 | 17, 18 | eqtrdi 2795 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → ((Base‘(Scalar‘𝑀)) ↑m ∅) =
{∅}) |
20 | 19 | raleqdv 3339 |
. . . 4
⊢ (𝑀 ∈ 𝑉 → (∀𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m
∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))) ↔ ∀𝑓 ∈ {∅} ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))))) |
21 | 14, 20 | mpbird 256 |
. . 3
⊢ (𝑀 ∈ 𝑉 → ∀𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m
∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))) |
22 | | 0elpw 5273 |
. . 3
⊢ ∅
∈ 𝒫 (Base‘𝑀) |
23 | 21, 22 | jctil 519 |
. 2
⊢ (𝑀 ∈ 𝑉 → (∅ ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))))) |
24 | | eqid 2738 |
. . . 4
⊢
(Base‘𝑀) =
(Base‘𝑀) |
25 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑀) = (0g‘𝑀) |
26 | | eqid 2738 |
. . . 4
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
27 | | eqid 2738 |
. . . 4
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
28 | | eqid 2738 |
. . . 4
⊢
(0g‘(Scalar‘𝑀)) =
(0g‘(Scalar‘𝑀)) |
29 | 24, 25, 26, 27, 28 | islininds 45675 |
. . 3
⊢ ((∅
∈ V ∧ 𝑀 ∈
𝑉) → (∅ linIndS
𝑀 ↔ (∅ ∈
𝒫 (Base‘𝑀)
∧ ∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))))) |
30 | 3, 29 | mpan 686 |
. 2
⊢ (𝑀 ∈ 𝑉 → (∅ linIndS 𝑀 ↔ (∅ ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))))) |
31 | 23, 30 | mpbird 256 |
1
⊢ (𝑀 ∈ 𝑉 → ∅ linIndS 𝑀) |