Metamath Proof Explorer

Theorem islinds5

Description: A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023)

Ref Expression
Hypotheses islinds5.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
islinds5.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
islinds5.r ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
islinds5.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
islinds5.z ⊢ 𝑂 = ( 0g ‘ 𝑊 )
islinds5.y ⊢ 0 = ( 0g ‘ 𝐹 )
Assertion islinds5 ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) ↔ ∀ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) )

Proof

Step Hyp Ref Expression
1 islinds5.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 islinds5.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 islinds5.r ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 islinds5.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 islinds5.z ⊢ 𝑂 = ( 0g ‘ 𝑊 )
6 islinds5.y ⊢ 0 = ( 0g ‘ 𝐹 )
7 1 islinds ⊢ ( 𝑊 ∈ LMod → ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑉 ⊆ 𝐵 ∧ ( I ↾ 𝑉 ) LIndF 𝑊 ) ) )
8 7 baibd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) ↔ ( I ↾ 𝑉 ) LIndF 𝑊 ) )
9 simpl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → 𝑊 ∈ LMod )
10 1 fvexi ⊢ 𝐵 ∈ V
11 10 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → 𝐵 ∈ V )
12 simpr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ⊆ 𝐵 )
13 11 12 ssexd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ V )
14 f1oi ⊢ ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉
15 f1of ⊢ ( ( I ↾ 𝑉 ) : 𝑉 –1-1-onto→ 𝑉 → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
16 14 15 mp1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝑉 )
17 16 12 fssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝐵 )
18 eqid ⊢ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) = ( Base ‘ ( 𝐹 freeLMod 𝑉 ) )
19 1 3 4 5 6 18 islindf4 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ∈ V ∧ ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝐵 ) → ( ( I ↾ 𝑉 ) LIndF 𝑊 ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
20 9 13 17 19 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( I ↾ 𝑉 ) LIndF 𝑊 ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
21 3 fvexi ⊢ 𝐹 ∈ V
22 eqid ⊢ ( 𝐹 freeLMod 𝑉 ) = ( 𝐹 freeLMod 𝑉 )
23 22 2 6 18 frlmelbas ⊢ ( ( 𝐹 ∈ V ∧ 𝑉 ∈ V ) → ( 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) )
24 21 13 23 sylancr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) )
25 24 imbi1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) → ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
26 elmapfn ⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → 𝑎 Fn 𝑉 )
27 26 ad2antrl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → 𝑎 Fn 𝑉 )
28 17 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( I ↾ 𝑉 ) : 𝑉 ⟶ 𝐵 )
29 28 ffnd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( I ↾ 𝑉 ) Fn 𝑉 )
30 13 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → 𝑉 ∈ V )
31 inidm ⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
32 eqidd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑎 ‘ 𝑣 ) = ( 𝑎 ‘ 𝑣 ) )
33 fvresi ⊢ ( 𝑣 ∈ 𝑉 → ( ( I ↾ 𝑉 ) ‘ 𝑣 ) = 𝑣 )
34 33 adantl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( I ↾ 𝑉 ) ‘ 𝑣 ) = 𝑣 )
35 27 29 30 30 31 32 34 offval ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) )
36 35 oveq2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) )
37 36 eqeq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 ↔ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) )
38 37 imbi1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) ) → ( ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ↔ ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
39 38 pm5.74da ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
40 impexp ⊢ ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
41 impexp ⊢ ( ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ↔ ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
42 41 imbi2i ⊢ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
43 40 42 bitr4i ⊢ ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
44 43 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
45 25 39 44 3bitrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ( 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) → ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) ) )
46 45 ralbidv2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( ∀ 𝑎 ∈ ( Base ‘ ( 𝐹 freeLMod 𝑉 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · ( I ↾ 𝑉 ) ) ) = 𝑂 → 𝑎 = ( 𝑉 × { 0 } ) ) ↔ ∀ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) )
47 8 20 46 3bitrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) ↔ ∀ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) = 𝑂 ) → 𝑎 = ( 𝑉 × { 0 } ) ) ) )