Metamath Proof Explorer

Theorem islindeps

Description: The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
islindeps.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
islindeps.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
islindeps.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
islindeps.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion islindeps ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) )

Proof

Step Hyp Ref Expression
1 islindeps.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 islindeps.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
3 islindeps.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
4 islindeps.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
5 islindeps.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 lindepsnlininds ⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀 ) )
7 6 ancoms ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀 ) )
8 1 2 3 4 5 islininds ⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
9 8 ancoms ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
10 ibar ⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
11 10 bicomd ⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
12 11 adantl ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
13 9 12 bitrd ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linIndS 𝑀 ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
14 13 notbid ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ¬ 𝑆 linIndS 𝑀 ↔ ¬ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
15 rexnal ⊢ ( ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ¬ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ¬ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
16 df-ne ⊢ ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑓 ‘ 𝑥 ) = 0 )
17 16 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ∃ 𝑥 ∈ 𝑆 ¬ ( 𝑓 ‘ 𝑥 ) = 0 )
18 rexnal ⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ ( 𝑓 ‘ 𝑥 ) = 0 ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 )
19 17 18 bitr2i ⊢ ( ¬ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ↔ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 )
20 19 anbi2i ⊢ ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
21 pm4.61 ⊢ ( ¬ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
22 df-3an ⊢ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
23 20 21 22 3bitr4i ⊢ ( ¬ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
24 23 rexbii ⊢ ( ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ¬ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
25 15 24 bitr3i ⊢ ( ¬ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
26 25 a1i ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ¬ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) )
27 7 14 26 3bitrd ⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) )