Metamath Proof Explorer

Theorem linds0

Description: The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion linds0 ⊢ M ∈ V → ∅ linIndS M

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
2 1 2a1i ⊢ M ∈ V → finSupp 0 Scalar ⁡ M ⁡ ∅ ∧ ∅ linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
3 0ex ⊢ ∅ ∈ V
4 breq1 ⊢ f = ∅ → finSupp 0 Scalar ⁡ M ⁡ f ↔ finSupp 0 Scalar ⁡ M ⁡ ∅
5 oveq1 ⊢ f = ∅ → f linC ⁡ M ∅ = ∅ linC ⁡ M ∅
6 5 eqeq1d ⊢ f = ∅ → f linC ⁡ M ∅ = 0 M ↔ ∅ linC ⁡ M ∅ = 0 M
7 4 6 anbi12d ⊢ f = ∅ → finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M ↔ finSupp 0 Scalar ⁡ M ⁡ ∅ ∧ ∅ linC ⁡ M ∅ = 0 M
8 fveq1 ⊢ f = ∅ → f ⁡ x = ∅ ⁡ x
9 8 eqeq1d ⊢ f = ∅ → f ⁡ x = 0 Scalar ⁡ M ↔ ∅ ⁡ x = 0 Scalar ⁡ M
10 9 ralbidv ⊢ f = ∅ → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M ↔ ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
11 7 10 imbi12d ⊢ f = ∅ → finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M ↔ finSupp 0 Scalar ⁡ M ⁡ ∅ ∧ ∅ linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
12 11 ralsng ⊢ ∅ ∈ V → ∀ f ∈ ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M ↔ finSupp 0 Scalar ⁡ M ⁡ ∅ ∧ ∅ linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
13 3 12 mp1i ⊢ M ∈ V → ∀ f ∈ ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M ↔ finSupp 0 Scalar ⁡ M ⁡ ∅ ∧ ∅ linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ ∅ ⁡ x = 0 Scalar ⁡ M
14 2 13 mpbird ⊢ M ∈ V → ∀ f ∈ ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
15 fvex ⊢ Base Scalar ⁡ M ∈ V
16 map0e ⊢ Base Scalar ⁡ M ∈ V → Base Scalar ⁡ M ∅ = 1 𝑜
17 15 16 mp1i ⊢ M ∈ V → Base Scalar ⁡ M ∅ = 1 𝑜
18 df1o2 ⊢ 1 𝑜 = ∅
19 17 18 eqtrdi ⊢ M ∈ V → Base Scalar ⁡ M ∅ = ∅
20 19 raleqdv ⊢ M ∈ V → ∀ f ∈ Base Scalar ⁡ M ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M ↔ ∀ f ∈ ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
21 14 20 mpbird ⊢ M ∈ V → ∀ f ∈ Base Scalar ⁡ M ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
22 0elpw ⊢ ∅ ∈ 𝒫 Base M
23 21 22 jctil ⊢ M ∈ V → ∅ ∈ 𝒫 Base M ∧ ∀ f ∈ Base Scalar ⁡ M ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
24 eqid ⊢ Base M = Base M
25 eqid ⊢ 0 M = 0 M
26 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
27 eqid ⊢ Base Scalar ⁡ M = Base Scalar ⁡ M
28 eqid ⊢ 0 Scalar ⁡ M = 0 Scalar ⁡ M
29 24 25 26 27 28 islininds ⊢ ∅ ∈ V ∧ M ∈ V → ∅ linIndS M ↔ ∅ ∈ 𝒫 Base M ∧ ∀ f ∈ Base Scalar ⁡ M ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
30 3 29 mpan ⊢ M ∈ V → ∅ linIndS M ↔ ∅ ∈ 𝒫 Base M ∧ ∀ f ∈ Base Scalar ⁡ M ∅ finSupp 0 Scalar ⁡ M ⁡ f ∧ f linC ⁡ M ∅ = 0 M → ∀ x ∈ ∅ f ⁡ x = 0 Scalar ⁡ M
31 23 30 mpbird ⊢ M ∈ V → ∅ linIndS M