Metamath Proof Explorer

Theorem ldepslinc

Description: For (left) vector spaces, isldepslvec2 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Assertion ldepslinc ( ∀ 𝑚 ∈ LVec ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∧ ¬ ∀ 𝑚 ∈ LMod ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑚 ) = ( Base ‘ 𝑚 )
2 eqid ⊢ ( 0g ‘ 𝑚 ) = ( 0g ‘ 𝑚 )
3 eqid ⊢ ( Scalar ‘ 𝑚 ) = ( Scalar ‘ 𝑚 )
4 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ ( Scalar ‘ 𝑚 ) )
5 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) )
6 1 2 3 4 5 isldepslvec2 ⊢ ( ( 𝑚 ∈ LVec ∧ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ↔ 𝑠 linDepS 𝑚 ) )
7 6 bicomd ⊢ ( ( 𝑚 ∈ LVec ∧ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
8 7 rgen2 ⊢ ∀ 𝑚 ∈ LVec ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
9 ldepsnlinc ⊢ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) )
10 df-ne ⊢ ( ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ↔ ¬ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 )
11 10 imbi2i ⊢ ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ¬ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
12 imnan ⊢ ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ¬ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ↔ ¬ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
13 11 12 bitri ⊢ ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ¬ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
14 13 ralbii ⊢ ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ¬ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
15 ralnex ⊢ ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ¬ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ↔ ¬ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
16 14 15 bitri ⊢ ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ¬ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
17 16 ralbii ⊢ ( ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑣 ∈ 𝑠 ¬ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
18 ralnex ⊢ ( ∀ 𝑣 ∈ 𝑠 ¬ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ↔ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
19 17 18 bitri ⊢ ( ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
20 19 anbi2i ⊢ ( ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ↔ ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
21 20 2rexbii ⊢ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ↔ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
22 9 21 mpbi ⊢ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
23 22 orci ⊢ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) )
24 r19.43 ⊢ ( ∃ 𝑚 ∈ LMod ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) )
25 23 24 mpbir ⊢ ∃ 𝑚 ∈ LMod ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) )
26 r19.43 ⊢ ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) )
27 26 rexbii ⊢ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ∃ 𝑚 ∈ LMod ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) )
28 25 27 mpbir ⊢ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) )
29 xor ⊢ ( ¬ ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ↔ ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) )
30 29 bicomi ⊢ ( ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ¬ ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
31 30 rexbii ⊢ ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ¬ ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
32 rexnal ⊢ ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ¬ ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ↔ ¬ ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
33 31 32 bitri ⊢ ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ¬ ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
34 33 rexbii ⊢ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ∃ 𝑚 ∈ LMod ¬ ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
35 rexnal ⊢ ( ∃ 𝑚 ∈ LMod ¬ ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ↔ ¬ ∀ 𝑚 ∈ LMod ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
36 34 35 bitri ⊢ ( ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( ( 𝑠 linDepS 𝑚 ∧ ¬ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∨ ( ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ∧ ¬ 𝑠 linDepS 𝑚 ) ) ↔ ¬ ∀ 𝑚 ∈ LMod ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )
37 28 36 mpbi ⊢ ¬ ∀ 𝑚 ∈ LMod ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) )
38 8 37 pm3.2i ⊢ ( ∀ 𝑚 ∈ LVec ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) ∧ ¬ ∀ 𝑚 ∈ LMod ∀ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ↔ ∃ 𝑣 ∈ 𝑠 ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = 𝑣 ) ) )