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	$⊢ R = Scalar (M)$
	lindslinind.b	$⊢ B = {Base}_{R}$
	lindslinind.0	$⊢ \underset{˙}{0} = 0_{R}$
	lindslinind.z	$⊢ Z = 0_{M}$
	lindslinind.y	$⊢ Y = {inv}_{g} (R) (f (x))$
	lindslinind.g	$⊢ G = {f ↾}_{(S ∖ \{x\})}$
Assertion	lindslinindimp2lem4	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S) \land (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x$

Proof

Step	Hyp	Ref	Expression
1		lindslinind.r	$⊢ R = Scalar (M)$
2		lindslinind.b	$⊢ B = {Base}_{R}$
3		lindslinind.0	$⊢ \underset{˙}{0} = 0_{R}$
4		lindslinind.z	$⊢ Z = 0_{M}$
5		lindslinind.y	$⊢ Y = {inv}_{g} (R) (f (x))$
6		lindslinind.g	$⊢ G = {f ↾}_{(S ∖ \{x\})}$
7		simpr	$⊢ (S \in V \land M \in LMod) \to M \in LMod$
8	7	adantr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to M \in LMod$
9		simprl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S \subseteq {Base}_{M}$
10		elpwg	$⊢ S \in V \to (S \in 𝒫 {Base}_{M} \leftrightarrow S \subseteq {Base}_{M})$
11	10	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (S \in 𝒫 {Base}_{M} \leftrightarrow S \subseteq {Base}_{M})$
12	9 11	mpbird	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S \in 𝒫 {Base}_{M}$
13		simpr	$⊢ (S \subseteq {Base}_{M} \land x \in S) \to x \in S$
14	13	adantl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to x \in S$
15	8 12 14	3jca	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (M \in LMod \land S \in 𝒫 {Base}_{M} \land x \in S)$
16	15	adantl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (M \in LMod \land S \in 𝒫 {Base}_{M} \land x \in S)$
17		simpl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f))$
18	6	a1i	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to G = {f ↾}_{(S ∖ \{x\})}$
19		eqid	$⊢ {Base}_{M} = {Base}_{M}$
20		eqid	$⊢ \cdot_{M} = \cdot_{M}$
21		eqid	$⊢ +_{M} = +_{M}$
22	19 1 2 20 21 3	lincdifsn	$⊢ ((M \in LMod \land S \in 𝒫 {Base}_{M} \land x \in S) \land (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land G = {f ↾}_{(S ∖ \{x\})}) \to f linC (M) S = (G linC (M) (S ∖ \{x\})) +_{M} (f (x) \cdot_{M} x)$
23	16 17 18 22	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to f linC (M) S = (G linC (M) (S ∖ \{x\})) +_{M} (f (x) \cdot_{M} x)$
24	23	eqeq1d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (f linC (M) S = Z \leftrightarrow (G linC (M) (S ∖ \{x\})) +_{M} (f (x) \cdot_{M} x) = Z)$
25		lmodgrp	$⊢ M \in LMod \to M \in Grp$
26	25	adantl	$⊢ (S \in V \land M \in LMod) \to M \in Grp$
27	26	ad2antrl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to M \in Grp$
28	7	ad2antrl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to M \in LMod$
29		elmapi	$⊢ f \in (B^{S}) \to f : S ⟶ B$
30		ffvelcdm	$⊢ (f : S ⟶ B \land x \in S) \to f (x) \in B$
31	30	expcom	$⊢ x \in S \to (f : S ⟶ B \to f (x) \in B)$
32	31	ad2antll	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (f : S ⟶ B \to f (x) \in B)$
33	29 32	syl5com	$⊢ f \in (B^{S}) \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to f (x) \in B)$
34	33	adantr	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to f (x) \in B)$
35	34	imp	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to f (x) \in B$
36		ssel2	$⊢ (S \subseteq {Base}_{M} \land x \in S) \to x \in {Base}_{M}$
37	36	ad2antll	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to x \in {Base}_{M}$
38	19 1 20 2	lmodvscl	$⊢ (M \in LMod \land f (x) \in B \land x \in {Base}_{M}) \to f (x) \cdot_{M} x \in {Base}_{M}$
39	28 35 37 38	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to f (x) \cdot_{M} x \in {Base}_{M}$
40		difexg	$⊢ S \in V \to S ∖ \{x\} \in V$
41	40	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \in V$
42		ssdifss	$⊢ S \subseteq {Base}_{M} \to S ∖ \{x\} \subseteq {Base}_{M}$
43	42	ad2antrl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \subseteq {Base}_{M}$
44	41 43	jca	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (S ∖ \{x\} \in V \land S ∖ \{x\} \subseteq {Base}_{M})$
45	44	adantl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (S ∖ \{x\} \in V \land S ∖ \{x\} \subseteq {Base}_{M})$
46		simprl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (S \in V \land M \in LMod)$
47		simpl	$⊢ (S \subseteq {Base}_{M} \land x \in S) \to S \subseteq {Base}_{M}$
48	47	ad2antll	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to S \subseteq {Base}_{M}$
49	13	ad2antll	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to x \in S$
50		simpl	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \to f \in (B^{S})$
51	50	adantr	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to f \in (B^{S})$
52	1 2 3 4 5 6	lindslinindimp2lem2	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to G \in (B^{(S ∖ \{x\})})$
53	46 48 49 51 52	syl13anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to G \in (B^{(S ∖ \{x\})})$
54		simpr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (S \subseteq {Base}_{M} \land x \in S)$
55	54	adantl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (S \subseteq {Base}_{M} \land x \in S)$
56	1 2 3 4 5 6	lindslinindimp2lem3	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S) \land (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f))) \to {finSupp}_{\underset{˙}{0}} (G)$
57	46 55 17 56	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to {finSupp}_{\underset{˙}{0}} (G)$
58	53 57	jca	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (G \in (B^{(S ∖ \{x\})}) \land {finSupp}_{\underset{˙}{0}} (G))$
59	19 1 2 3	lincfsuppcl	$⊢ (M \in LMod \land (S ∖ \{x\} \in V \land S ∖ \{x\} \subseteq {Base}_{M}) \land (G \in (B^{(S ∖ \{x\})}) \land {finSupp}_{\underset{˙}{0}} (G))) \to G linC (M) (S ∖ \{x\}) \in {Base}_{M}$
60	28 45 58 59	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to G linC (M) (S ∖ \{x\}) \in {Base}_{M}$
61		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
62	19 21 4 61	grpinvid2	$⊢ (M \in Grp \land f (x) \cdot_{M} x \in {Base}_{M} \land G linC (M) (S ∖ \{x\}) \in {Base}_{M}) \to ({inv}_{g} (M) (f (x) \cdot_{M} x) = G linC (M) (S ∖ \{x\}) \leftrightarrow (G linC (M) (S ∖ \{x\})) +_{M} (f (x) \cdot_{M} x) = Z)$
63	27 39 60 62	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to ({inv}_{g} (M) (f (x) \cdot_{M} x) = G linC (M) (S ∖ \{x\}) \leftrightarrow (G linC (M) (S ∖ \{x\})) +_{M} (f (x) \cdot_{M} x) = Z)$
64	24 63	bitr4d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (f linC (M) S = Z \leftrightarrow {inv}_{g} (M) (f (x) \cdot_{M} x) = G linC (M) (S ∖ \{x\}))$
65		eqcom	$⊢ {inv}_{g} (M) (f (x) \cdot_{M} x) = G linC (M) (S ∖ \{x\}) \leftrightarrow G linC (M) (S ∖ \{x\}) = {inv}_{g} (M) (f (x) \cdot_{M} x)$
66	1	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
67	2 66	eqtri	$⊢ B = {Base}_{Scalar (M)}$
68	67	oveq1i	$⊢ B^{(S ∖ \{x\})} = {Base}_{Scalar (M)}^{(S ∖ \{x\})}$
69	53 68	eleqtrdi	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to G \in ({Base}_{Scalar (M)}^{(S ∖ \{x\})})$
70	41 43	elpwd	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \in 𝒫 {Base}_{M}$
71	70	adantl	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to S ∖ \{x\} \in 𝒫 {Base}_{M}$
72		lincval	$⊢ (M \in LMod \land G \in ({Base}_{Scalar (M)}^{(S ∖ \{x\})}) \land S ∖ \{x\} \in 𝒫 {Base}_{M}) \to G linC (M) (S ∖ \{x\}) = \underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y)$
73	28 69 71 72	syl3anc	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to G linC (M) (S ∖ \{x\}) = \underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y)$
74	73	eqeq1d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (G linC (M) (S ∖ \{x\}) = {inv}_{g} (M) (f (x) \cdot_{M} x) \leftrightarrow \underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y) = {inv}_{g} (M) (f (x) \cdot_{M} x))$
75	6	fveq1i	$⊢ G (y) = ({f ↾}_{(S ∖ \{x\})}) (y)$
76	75	a1i	$⊢ (((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \land y \in (S ∖ \{x\})) \to G (y) = ({f ↾}_{(S ∖ \{x\})}) (y)$
77		fvres	$⊢ y \in (S ∖ \{x\}) \to ({f ↾}_{(S ∖ \{x\})}) (y) = f (y)$
78	77	adantl	$⊢ (((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \land y \in (S ∖ \{x\})) \to ({f ↾}_{(S ∖ \{x\})}) (y) = f (y)$
79	76 78	eqtrd	$⊢ (((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \land y \in (S ∖ \{x\})) \to G (y) = f (y)$
80	79	oveq1d	$⊢ (((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \land y \in (S ∖ \{x\})) \to G (y) \cdot_{M} y = f (y) \cdot_{M} y$
81	80	mpteq2dva	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (y \in (S ∖ \{x\}) ⟼ G (y) \cdot_{M} y) = (y \in (S ∖ \{x\}) ⟼ f (y) \cdot_{M} y)$
82	81	oveq2d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y) = \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y)$
83		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
84	19 1 20 61 2 83 28 37 35	lmodvsneg	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to {inv}_{g} (M) (f (x) \cdot_{M} x) = {inv}_{g} (R) (f (x)) \cdot_{M} x$
85	5	eqcomi	$⊢ {inv}_{g} (R) (f (x)) = Y$
86	85	a1i	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to {inv}_{g} (R) (f (x)) = Y$
87	86	oveq1d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to {inv}_{g} (R) (f (x)) \cdot_{M} x = Y \cdot_{M} x$
88	84 87	eqtrd	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to {inv}_{g} (M) (f (x) \cdot_{M} x) = Y \cdot_{M} x$
89	82 88	eqeq12d	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (\underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y) = {inv}_{g} (M) (f (x) \cdot_{M} x) \leftrightarrow \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
90	89	biimpd	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (\underset{y \in S ∖ \{x\}}{\sum_{M}} (G (y) \cdot_{M} y) = {inv}_{g} (M) (f (x) \cdot_{M} x) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
91	74 90	sylbid	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (G linC (M) (S ∖ \{x\}) = {inv}_{g} (M) (f (x) \cdot_{M} x) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
92	65 91	biimtrid	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to ({inv}_{g} (M) (f (x) \cdot_{M} x) = G linC (M) (S ∖ \{x\}) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
93	64 92	sylbid	$⊢ ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \land ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S))) \to (f linC (M) S = Z \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
94	93	ex	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (f linC (M) S = Z \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x))$
95	94	com23	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f)) \to (f linC (M) S = Z \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x))$
96	95	3impia	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
97	96	com12	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to ((f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x)$
98	97	3impia	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S) \land (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to \underset{y \in S ∖ \{x\}}{\sum_{M}} (f (y) \cdot_{M} y) = Y \cdot_{M} x$

Metamath Proof Explorer

Theorem lindslinindimp2lem4

Proof