Metamath Proof Explorer

Theorem lindslinindsimp2

Description: Implication 2 for lindslininds . (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses lindslinind.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
lindslinind.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
lindslinind.0 ⊢ 0 = ( 0g ‘ 𝑅 )
lindslinind.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
Assertion lindslinindsimp2 ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 lindslinind.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
2 lindslinind.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 lindslinind.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 lindslinind.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
5 simprl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
6 elpwg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) )
7 6 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) )
8 5 7 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) → 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) )
9 simplr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LMod )
10 ssdifss ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) )
11 10 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) )
12 difexg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∖ { 𝑠 } ) ∈ V )
13 12 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ V )
14 elpwg ⊢ ( ( 𝑆 ∖ { 𝑠 } ) ∈ V → ( ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) ) )
15 13 14 syl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) ) )
16 11 15 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
17 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18 17 lspeqlco ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) = ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) )
19 18 eleq2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) )
20 19 bicomd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ) )
21 9 16 20 syl2anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ) )
22 21 notbid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ) )
23 17 1 2 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
24 3 eqcomi ⊢ ( 0g ‘ 𝑅 ) = 0
25 24 breq2i ⊢ ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ↔ 𝑔 finSupp 0 )
26 25 anbi1i ⊢ ( ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
27 26 rexbii ⊢ ( ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
28 27 anbi2i ⊢ ( ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
29 23 28 bitrdi ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
30 9 16 29 syl2anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
31 30 notbid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ¬ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
32 ianor ⊢ ( ¬ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
33 ralnex ⊢ ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
34 ianor ⊢ ( ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
35 34 ralbii ⊢ ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
36 33 35 bitr3i ⊢ ( ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
37 36 orbi2i ⊢ ( ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
38 32 37 bitri ⊢ ( ¬ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
39 31 38 bitrdi ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
40 22 39 bitrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
41 40 2ralbidv ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
42 simpllr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑀 ∈ LMod )
43 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
44 43 adantl ⊢ ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑦 ∈ 𝐵 )
45 44 adantl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑦 ∈ 𝐵 )
46 ssel2 ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ ( Base ‘ 𝑀 ) )
47 46 ad2ant2lr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑠 ∈ ( Base ‘ 𝑀 ) )
48 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
49 17 1 48 2 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑦 ∈ 𝐵 ∧ 𝑠 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) )
50 42 45 47 49 syl3anc ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) )
51 50 notnotd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ¬ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) )
52 nbfal ⊢ ( ¬ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ↔ ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ↔ ⊥ ) )
53 51 52 sylib ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ↔ ⊥ ) )
54 53 orbi1d ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
55 54 2ralbidva ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
56 r19.32v ⊢ ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ⊥ ∨ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
57 56 ralbii ⊢ ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ∀ 𝑠 ∈ 𝑆 ( ⊥ ∨ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
58 r19.32v ⊢ ( ∀ 𝑠 ∈ 𝑆 ( ⊥ ∨ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ⊥ ∨ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
59 57 58 bitri ⊢ ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ⊥ ∨ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
60 falim ⊢ ( ⊥ → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
61 sneq ⊢ ( 𝑠 = 𝑥 → { 𝑠 } = { 𝑥 } )
62 61 difeq2d ⊢ ( 𝑠 = 𝑥 → ( 𝑆 ∖ { 𝑠 } ) = ( 𝑆 ∖ { 𝑥 } ) )
63 62 oveq2d ⊢ ( 𝑠 = 𝑥 → ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) = ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
64 oveq2 ⊢ ( 𝑠 = 𝑥 → ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
65 62 oveq2d ⊢ ( 𝑠 = 𝑥 → ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) )
66 64 65 eqeq12d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
67 66 notbid ⊢ ( 𝑠 = 𝑥 → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ↔ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
68 67 orbi2d ⊢ ( 𝑠 = 𝑥 → ( ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
69 63 68 raleqbidv ⊢ ( 𝑠 = 𝑥 → ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
70 69 ralbidv ⊢ ( 𝑠 = 𝑥 → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
71 70 rspcva ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
72 1 2 3 4 lindslinindsimp2lem5 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
73 72 expr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑥 ∈ 𝑆 → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
74 73 com14 ⊢ ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑥 ∈ 𝑆 → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
75 71 74 syl ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( 𝑥 ∈ 𝑆 → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
76 75 ex ⊢ ( 𝑥 ∈ 𝑆 → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) → ( 𝑥 ∈ 𝑆 → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ) )
77 76 pm2.43a ⊢ ( 𝑥 ∈ 𝑆 → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
78 77 com14 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑥 ∈ 𝑆 → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
79 78 imp ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑥 ∈ 𝑆 → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
80 79 expdimp ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( 𝑥 ∈ 𝑆 → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
81 80 ralrimdv ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
82 81 ralrimiva ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
83 82 expcom ⊢ ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
84 60 83 jaoi ⊢ ( ( ⊥ ∨ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
85 84 com12 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ( ⊥ ∨ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
86 59 85 syl5bi ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ⊥ ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
87 55 86 sylbid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∨ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
88 41 87 sylbid ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
89 88 impr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
90 8 89 jca ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
91 90 ex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )