| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ral0 4513 | . . . . . 6
⊢
∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)) | 
| 2 | 1 | 2a1i 12 | . . . . 5
⊢ (𝑀 ∈ 𝑉 → ((∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀))
→ ∀𝑥 ∈
∅ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)))) | 
| 3 |  | 0ex 5307 | . . . . . 6
⊢ ∅
∈ V | 
| 4 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ↔ ∅ finSupp
(0g‘(Scalar‘𝑀)))) | 
| 5 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑓 = ∅ → (𝑓( linC ‘𝑀)∅) = (∅( linC ‘𝑀)∅)) | 
| 6 | 5 | eqeq1d 2739 | . . . . . . . . 9
⊢ (𝑓 = ∅ → ((𝑓( linC ‘𝑀)∅) = (0g‘𝑀) ↔ (∅( linC
‘𝑀)∅) =
(0g‘𝑀))) | 
| 7 | 4, 6 | anbi12d 632 | . . . . . . . 8
⊢ (𝑓 = ∅ → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) ↔ (∅ finSupp
(0g‘(Scalar‘𝑀)) ∧ (∅( linC ‘𝑀)∅) =
(0g‘𝑀)))) | 
| 8 |  | fveq1 6905 | . . . . . . . . . 10
⊢ (𝑓 = ∅ → (𝑓‘𝑥) = (∅‘𝑥)) | 
| 9 | 8 | eqeq1d 2739 | . . . . . . . . 9
⊢ (𝑓 = ∅ → ((𝑓‘𝑥) = (0g‘(Scalar‘𝑀)) ↔ (∅‘𝑥) =
(0g‘(Scalar‘𝑀)))) | 
| 10 | 9 | ralbidv 3178 | . . . . . . . 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 4675 | . . . . . 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 257 | . . . 4
⊢ (𝑀 ∈ 𝑉 → ∀𝑓 ∈ {∅} ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))) | 
| 15 |  | fvex 6919 | . . . . . 6
⊢
(Base‘(Scalar‘𝑀)) ∈ V | 
| 16 |  | map0e 8922 | . . . . . 6
⊢
((Base‘(Scalar‘𝑀)) ∈ V →
((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) | 
| 17 | 15, 16 | mp1i 13 | . . . . 5
⊢ (𝑀 ∈ 𝑉 → ((Base‘(Scalar‘𝑀)) ↑m ∅) =
1o) | 
| 18 |  | df1o2 8513 | . . . . 5
⊢
1o = {∅} | 
| 19 | 17, 18 | eqtrdi 2793 | . . . 4
⊢ (𝑀 ∈ 𝑉 → ((Base‘(Scalar‘𝑀)) ↑m ∅) =
{∅}) | 
| 20 | 14, 19 | raleqtrrdv 3330 | . . 3
⊢ (𝑀 ∈ 𝑉 → ∀𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m
∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))) | 
| 21 |  | 0elpw 5356 | . . 3
⊢ ∅
∈ 𝒫 (Base‘𝑀) | 
| 22 | 20, 21 | jctil 519 | . 2
⊢ (𝑀 ∈ 𝑉 → (∅ ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀))))) | 
| 23 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 24 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 25 |  | eqid 2737 | . . . 4
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) | 
| 26 |  | eqid 2737 | . . . 4
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) | 
| 27 |  | eqid 2737 | . . . 4
⊢
(0g‘(Scalar‘𝑀)) =
(0g‘(Scalar‘𝑀)) | 
| 28 | 23, 24, 25, 26, 27 | islininds 48363 | . . 3
⊢ ((∅
∈ V ∧ 𝑀 ∈
𝑉) → (∅ linIndS
𝑀 ↔ (∅ ∈
𝒫 (Base‘𝑀)
∧ ∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))))) | 
| 29 | 3, 28 | mpan 690 | . 2
⊢ (𝑀 ∈ 𝑉 → (∅ linIndS 𝑀 ↔ (∅ ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m ∅)((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)∅) = (0g‘𝑀)) → ∀𝑥 ∈ ∅ (𝑓‘𝑥) = (0g‘(Scalar‘𝑀)))))) | 
| 30 | 22, 29 | mpbird 257 | 1
⊢ (𝑀 ∈ 𝑉 → ∅ linIndS 𝑀) |