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 syl6eq 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