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→∅linIndSM

Proof

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