Metamath Proof Explorer

Theorem lindslinindsimp2lem5

Description: Lemma 5 for lindslinindsimp2 . (Contributed by AV, 25-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 lindslinindsimp2lem5 ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑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 ax-1 ⊢ ( ( 𝑓 ‘ 𝑥 ) = 0 → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
6 5 2a1d ⊢ ( ( 𝑓 ‘ 𝑥 ) = 0 → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
7 elmapi ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝐵 )
8 ffvelcdm ⊢ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
9 8 expcom ⊢ ( 𝑥 ∈ 𝑆 → ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
10 9 adantl ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
11 10 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
12 11 com12 ⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
13 7 12 syl ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
14 13 adantr ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
15 14 impcom ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
16 15 biantrurd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) )
17 df-ne ⊢ ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑓 ‘ 𝑥 ) = 0 )
18 17 bicomi ⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) = 0 ↔ ( 𝑓 ‘ 𝑥 ) ≠ 0 )
19 eldifsn ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) )
20 16 18 19 3bitr4g ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ¬ ( 𝑓 ‘ 𝑥 ) = 0 ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) ) )
21 1 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
22 21 adantl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → 𝑅 ∈ Grp )
23 22 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑅 ∈ Grp )
24 23 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑅 ∈ Grp )
25 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
26 2 3 25 grpinvnzcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) )
27 24 26 sylan ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) )
28 27 ex ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) ) )
29 20 28 sylbid ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ¬ ( 𝑓 ‘ 𝑥 ) = 0 → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) ) )
30 oveq1 ⊢ ( 𝑦 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
31 30 eqeq1d ⊢ ( 𝑦 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
32 31 notbid ⊢ ( 𝑦 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
33 32 orbi2d ⊢ ( 𝑦 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
34 33 ralbidv ⊢ ( 𝑦 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) → ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
35 34 rspcva ⊢ ( ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) → ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
36 simpl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) )
37 36 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) )
38 simplrl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
39 simplrr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑥 ∈ 𝑆 )
40 simpl ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) )
41 40 adantl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) )
42 eqid ⊢ ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) )
43 eqid ⊢ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) )
44 1 2 3 4 42 43 lindslinindimp2lem2 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
45 37 38 39 41 44 syl13anc ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
46 id ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) )
47 3 a1i ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → 0 = ( 0g ‘ 𝑅 ) )
48 46 47 breq12d ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝑔 finSupp 0 ↔ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) ) )
49 48 notbid ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( ¬ 𝑔 finSupp 0 ↔ ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) ) )
50 oveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) )
51 50 eqeq2d ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
52 51 notbid ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
53 49 52 orbi12d ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
54 53 rspcva ⊢ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) → ( ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
55 3 breq2i ⊢ ( 𝑓 finSupp 0 ↔ 𝑓 finSupp ( 0g ‘ 𝑅 ) )
56 55 biimpi ⊢ ( 𝑓 finSupp 0 → 𝑓 finSupp ( 0g ‘ 𝑅 ) )
57 56 adantr ⊢ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → 𝑓 finSupp ( 0g ‘ 𝑅 ) )
58 57 adantl ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → 𝑓 finSupp ( 0g ‘ 𝑅 ) )
59 58 adantl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑓 finSupp ( 0g ‘ 𝑅 ) )
60 fvexd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 0g ‘ 𝑅 ) ∈ V )
61 59 60 fsuppres ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) )
62 61 pm2.24d ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
63 62 com12 ⊢ ( ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
64 simplr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑀 ∈ LMod )
65 64 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → 𝑀 ∈ LMod )
66 1 fveq2i ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
67 2 66 eqtr2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = 𝐵
68 67 oveq1i ⊢ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) )
69 45 68 eleqtrrdi ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
70 ssdifss ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) )
71 70 adantr ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) )
72 71 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) )
73 difexg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
74 73 adantr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
75 74 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
76 elpwg ⊢ ( ( 𝑆 ∖ { 𝑥 } ) ∈ V → ( ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) ) )
77 75 76 syl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) ) )
78 72 77 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
79 78 adantr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
80 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
81 65 69 79 80 syl3anc ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
82 fvres ⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) = ( 𝑓 ‘ 𝑧 ) )
83 82 adantl ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) = ( 𝑓 ‘ 𝑧 ) )
84 83 oveq1d ⊢ ( ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) = ( ( 𝑓 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) )
85 84 mpteq2dva ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) )
86 85 oveq2d ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
87 simplr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) )
88 3anass ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ↔ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) )
89 88 bicomi ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ↔ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
90 89 biimpi ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
91 90 adantl ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
92 1 2 3 4 42 43 lindslinindimp2lem4 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
93 37 87 91 92 syl3anc ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
94 81 86 93 3eqtrrd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) )
95 94 pm2.24d ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
96 95 com12 ⊢ ( ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
97 63 96 jaoi ⊢ ( ( ¬ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp ( 0g ‘ 𝑅 ) ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
98 54 97 syl ⊢ ( ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
99 98 ex ⊢ ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) → ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
100 99 com23 ⊢ ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
101 45 100 mpcom ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
102 35 101 syl5 ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) )
103 102 expd ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝐵 ∖ { 0 } ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
104 29 103 syldc ⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) = 0 → ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
105 104 expd ⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) = 0 → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
106 6 105 pm2.61i ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑔 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ( ¬ 𝑔 finSupp 0 ∨ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑔 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 ) ) )