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 ( 𝑀 ∈ 𝑉 → ∅ linIndS 𝑀 )

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
2 1 2a1i ⊢ ( 𝑀 ∈ 𝑉 → ( ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
3 0ex ⊢ ∅ ∈ V
4 breq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
5 oveq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( ∅ ( linC ‘ 𝑀 ) ∅ ) )
6 5 eqeq1d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ↔ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) )
7 4 6 anbi12d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) ↔ ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) ) )
8 fveq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 ‘ 𝑥 ) = ( ∅ ‘ 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
10 9 ralbidv ⊢ ( 𝑓 = ∅ → ( ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
11 7 10 imbi12d ⊢ ( 𝑓 = ∅ → ( ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
12 11 ralsng ⊢ ( ∅ ∈ V → ( ∀ 𝑓 ∈ { ∅ } ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
13 3 12 mp1i ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑓 ∈ { ∅ } ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( ∅ ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
14 2 13 mpbird ⊢ ( 𝑀 ∈ 𝑉 → ∀ 𝑓 ∈ { ∅ } ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
16 map0e ⊢ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
17 15 16 mp1i ⊢ ( 𝑀 ∈ 𝑉 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
18 df1o2 ⊢ 1o = { ∅ }
19 17 18 eqtrdi ⊢ ( 𝑀 ∈ 𝑉 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = { ∅ } )
20 14 19 raleqtrrdv ⊢ ( 𝑀 ∈ 𝑉 → ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
21 0elpw ⊢ ∅ ∈ 𝒫 ( Base ‘ 𝑀 )
22 20 21 jctil ⊢ ( 𝑀 ∈ 𝑉 → ( ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
23 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
24 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
25 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
26 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
27 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
28 23 24 25 26 27 islininds ⊢ ( ( ∅ ∈ V ∧ 𝑀 ∈ 𝑉 ) → ( ∅ linIndS 𝑀 ↔ ( ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) )
29 3 28 mpan ⊢ ( 𝑀 ∈ 𝑉 → ( ∅ linIndS 𝑀 ↔ ( ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ∅ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) )
30 22 29 mpbird ⊢ ( 𝑀 ∈ 𝑉 → ∅ linIndS 𝑀 )