Metamath Proof Explorer

Theorem lindslinindsimp1

Description: Implication 1 for lindslininds . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019) (Proof shortened by II, 16-Feb-2023)

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

Proof

Step Hyp Ref Expression
1 lindslinind.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
2 lindslinind.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 lindslinind.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 lindslinind.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
5 elpwi ⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
6 5 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
7 simpr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → 𝑀 ∈ LMod )
8 7 anim2i ⊢ ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) )
9 8 ancomd ⊢ ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
10 9 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
11 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
12 11 adantl ⊢ ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑦 ∈ 𝐵 )
13 12 adantl ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑦 ∈ 𝐵 )
14 13 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → 𝑦 ∈ 𝐵 )
15 simprl ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑠 ∈ 𝑆 )
16 15 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → 𝑠 ∈ 𝑆 )
17 simprl ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) )
18 14 16 17 3jca ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) )
19 simprrl ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → 𝑔 finSupp 0 )
20 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
21 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
22 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) )
23 20 1 2 3 4 21 22 lincext2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ 𝑔 finSupp 0 ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 )
24 10 18 19 23 syl3anc ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 )
25 8 adantr ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) )
26 25 ancomd ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
27 26 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
28 20 1 2 3 4 21 22 lincext1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ∈ ( 𝐵 ↑m 𝑆 ) )
29 27 18 28 syl2anc ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ∈ ( 𝐵 ↑m 𝑆 ) )
30 breq1 ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ) )
31 oveq1 ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) )
32 31 eqeq1d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
33 30 32 anbi12d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) )
34 fveq1 ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) )
35 34 eqeq1d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) )
36 35 ralbidv ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) )
37 33 36 imbi12d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) ) )
38 37 rspcv ⊢ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ∈ ( 𝐵 ↑m 𝑆 ) → ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) ) )
39 29 38 syl ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) ) )
40 39 exp4a ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) ) ) )
41 24 40 mpid ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) ) )
42 simprr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
43 20 1 2 3 4 21 22 lincext3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
44 10 18 42 43 syl3anc ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
45 fveqeq2 ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = 0 ) )
46 45 rspcv ⊢ ( 𝑠 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = 0 ) )
47 16 46 syl ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = 0 ) )
48 eqidd ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) )
49 iftrue ⊢ ( 𝑧 = 𝑠 → if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) = ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) )
50 49 adantl ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑧 = 𝑠 ) → if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) = ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) )
51 fvexd ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ V )
52 48 50 15 51 fvmptd ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) )
53 52 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) )
54 53 eqeq1d ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = 0 ↔ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 ) )
55 1 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
56 2 3 21 grpinvnzcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
57 eldif ⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ 𝐵 ∧ ¬ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 0 } ) )
58 fvex ⊢ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ V
59 58 elsn ⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 0 } ↔ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 )
60 pm2.21 ⊢ ( ¬ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
61 60 com25 ⊢ ( ¬ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
62 59 61 sylnbi ⊢ ( ¬ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 0 } → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
63 57 62 simplbiim ⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
64 56 63 syl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
65 64 ex ⊢ ( 𝑅 ∈ Grp → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) ) )
66 55 65 syl ⊢ ( 𝑀 ∈ LMod → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∈ 𝑉 → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) ) )
67 66 com24 ⊢ ( 𝑀 ∈ LMod → ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) ) )
68 67 impcom ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
69 68 impcom ⊢ ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑠 ∈ 𝑆 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
70 69 com13 ⊢ ( 𝑠 ∈ 𝑆 → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
71 70 imp ⊢ ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
72 71 impcom ⊢ ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
73 72 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
74 54 73 sylbid ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
75 47 74 syld ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
76 44 75 embantd ⊢ ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ( ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) , ( 𝑔 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = 0 ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
77 41 76 syldc ⊢ ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
78 77 exp5j ⊢ ( ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) ) )
79 78 impcom ⊢ ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
80 79 impcom ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
81 80 imp ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ∧ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
82 81 expdimp ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
83 82 expd ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) → ( 𝑔 finSupp 0 → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
84 83 impcom ⊢ ( ( 𝑔 finSupp 0 ∧ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
85 84 pm2.01d ⊢ ( ( 𝑔 finSupp 0 ∧ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) )
86 85 olcd ⊢ ( ( 𝑔 finSupp 0 ∧ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
87 animorl ⊢ ( ( ¬ 𝑔 finSupp 0 ∧ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
88 86 87 pm2.61ian ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) ∧ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
89 88 ralrimiva ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
90 ralnex ⊢ ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
91 ianor ⊢ ( ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
92 91 ralbii ⊢ ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
93 90 92 bitr3i ⊢ ( ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
94 89 93 sylibr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ¬ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
95 94 intnand ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ¬ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
96 7 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → 𝑀 ∈ LMod )
97 difexg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∖ { 𝑠 } ) ∈ V )
98 97 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ V )
99 5 ssdifssd ⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) )
100 99 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑆 ∖ { 𝑠 } ) ⊆ ( Base ‘ 𝑀 ) )
101 98 100 elpwd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
102 101 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
103 20 lspeqlco ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) = ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) )
104 103 eleq2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) )
105 104 bicomd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ) )
106 96 102 105 syl2anc ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ) )
107 7 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → 𝑀 ∈ LMod )
108 difexg ⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑠 } ) ∈ V )
109 108 99 elpwd ⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
110 109 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
111 107 110 jca ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
112 111 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
113 20 1 2 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
114 3 eqcomi ⊢ ( 0g ‘ 𝑅 ) = 0
115 114 breq2i ⊢ ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ↔ 𝑔 finSupp 0 )
116 115 anbi1i ⊢ ( ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
117 116 rexbii ⊢ ( ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ↔ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) )
118 117 anbi2i ⊢ ( ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
119 113 118 bitrdi ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑠 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
120 112 119 syl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( 𝑀 LinCo ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
121 106 120 bitrd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑔 finSupp 0 ∧ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) ) )
122 95 121 mtbird ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) )
123 122 ralrimivva ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) )
124 6 123 jca ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) )
125 124 ex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )