lindslinindimp2lem3

Description: Lemma 3 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019)

	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	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)$

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		simp3r	$⊢ ((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}} (f)$
8	3	fvexi	$⊢ \underset{˙}{0} \in V$
9	8	a1i	$⊢ ((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 \underset{˙}{0} \in V$
10	7 9	fsuppres	$⊢ ((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}} (({f ↾}_{(S ∖ \{x\})}))$
11	6 10	eqbrtrid	$⊢ ((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)$

Metamath Proof Explorer