Metamath Proof Explorer

Theorem lindslinindimp2lem4

Description: Lemma 4 for lindslinindsimp2 . (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 ‘ 𝑀 )
lindslinind.y ⊢ 𝑌 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) )
lindslinind.g ⊢ 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) )
Assertion lindslinindimp2lem4 ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )

Proof

Step Hyp Ref Expression
1 lindslinind.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
2 lindslinind.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 lindslinind.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 lindslinind.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
5 lindslinind.y ⊢ 𝑌 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) )
6 lindslinind.g ⊢ 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) )
7 simpr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → 𝑀 ∈ LMod )
8 7 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑀 ∈ LMod )
9 simprl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
10 elpwg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) )
11 10 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) )
12 9 11 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) )
13 simpr ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
14 13 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
15 8 12 14 3jca ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) )
16 15 adantl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) )
17 simpl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) )
18 6 a1i ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) )
19 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
20 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
21 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
22 19 1 2 20 21 3 lincdifsn ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ( +g ‘ 𝑀 ) ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
23 16 17 18 22 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ( +g ‘ 𝑀 ) ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
24 23 eqeq1d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ↔ ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ( +g ‘ 𝑀 ) ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = 𝑍 ) )
25 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
26 25 adantl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → 𝑀 ∈ Grp )
27 26 ad2antrl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑀 ∈ Grp )
28 7 ad2antrl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑀 ∈ LMod )
29 elmapi ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝐵 )
30 ffvelcdm ⊢ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
31 30 expcom ⊢ ( 𝑥 ∈ 𝑆 → ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
32 31 ad2antll ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
33 29 32 syl5com ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
34 33 adantr ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
35 34 imp ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
36 ssel2 ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
37 36 ad2antll ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
38 19 1 20 2 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
39 28 35 37 38 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
40 difexg ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
41 40 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
42 ssdifss ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) )
43 42 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) )
44 41 43 jca ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑆 ∖ { 𝑥 } ) ∈ V ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) ) )
45 44 adantl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑆 ∖ { 𝑥 } ) ∈ V ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) ) )
46 simprl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) )
47 simpl ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
48 47 ad2antll ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
49 13 ad2antll ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑥 ∈ 𝑆 )
50 simpl ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) → 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) )
51 50 adantr ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) )
52 1 2 3 4 5 6 lindslinindimp2lem2 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
53 46 48 49 51 52 syl13anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
54 simpr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) )
55 54 adantl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) )
56 1 2 3 4 5 6 lindslinindimp2lem3 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → 𝐺 finSupp 0 )
57 46 55 17 56 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝐺 finSupp 0 )
58 53 57 jca ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝐺 finSupp 0 ) )
59 19 1 2 3 lincfsuppcl ⊢ ( ( 𝑀 ∈ LMod ∧ ( ( 𝑆 ∖ { 𝑥 } ) ∈ V ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑀 ) ) ∧ ( 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝐺 finSupp 0 ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Base ‘ 𝑀 ) )
60 28 45 58 59 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Base ‘ 𝑀 ) )
61 eqid ⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
62 19 21 4 61 grpinvid2 ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) ∧ ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Base ‘ 𝑀 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ( +g ‘ 𝑀 ) ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = 𝑍 ) )
63 27 39 60 62 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ( +g ‘ 𝑀 ) ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = 𝑍 ) )
64 24 63 bitr4d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ↔ ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ) )
65 eqcom ⊢ ( ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
66 1 fveq2i ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
67 2 66 eqtri ⊢ 𝐵 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
68 67 oveq1i ⊢ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) )
69 53 68 eleqtrdi ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) ) )
70 41 43 elpwd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
71 70 adantl ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
72 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑥 } ) ) ∧ ( 𝑆 ∖ { 𝑥 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
73 28 69 71 72 syl3anc ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
74 73 eqeq1d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ↔ ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
75 6 fveq1i ⊢ ( 𝐺 ‘ 𝑦 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑦 )
76 75 a1i ⊢ ( ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑦 ) )
77 fvres ⊢ ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
78 77 adantl ⊢ ( ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
79 76 78 eqtrd ⊢ ( ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
80 79 oveq1d ⊢ ( ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
81 80 mpteq2dva ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) )
82 81 oveq2d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
83 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
84 19 1 20 61 2 83 28 37 35 lmodvsneg ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
85 5 eqcomi ⊢ ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑌
86 85 a1i ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑌 )
87 86 oveq1d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
88 84 87 eqtrd ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
89 82 88 eqeq12d ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ↔ ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
90 89 biimpd ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝐺 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
91 74 90 sylbid ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) = ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
92 65 91 biimtrid ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( ( invg ‘ 𝑀 ) ‘ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑥 } ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
93 64 92 sylbid ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
94 93 ex ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
95 94 com23 ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
96 95 3impia ⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
97 96 com12 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
98 97 3impia ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) → ( 𝑀 Σg ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )