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 ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )