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 ( 𝑦 ∈ ( 𝑆 ∖ { 𝑥 } ) ↦ ( ( 𝑓 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )