lindslinindimp2lem1

Description: Lemma 1 for lindslinindsimp2 . (Contributed by AV, 25-Apr-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	lindslinindimp2lem1	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to Y \in B$

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	1	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
8	7	adantl	$⊢ (S \in V \land M \in LMod) \to R \in Grp$
9		elmapi	$⊢ f \in (B^{S}) \to f : S ⟶ B$
10		ffvelrn	$⊢ (f : S ⟶ B \land x \in S) \to f (x) \in B$
11	10	a1d	$⊢ (f : S ⟶ B \land x \in S) \to (S \subseteq {Base}_{M} \to f (x) \in B)$
12	11	ex	$⊢ f : S ⟶ B \to (x \in S \to (S \subseteq {Base}_{M} \to f (x) \in B))$
13	9 12	syl	$⊢ f \in (B^{S}) \to (x \in S \to (S \subseteq {Base}_{M} \to f (x) \in B))$
14	13	com13	$⊢ S \subseteq {Base}_{M} \to (x \in S \to (f \in (B^{S}) \to f (x) \in B))$
15	14	3imp	$⊢ (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S})) \to f (x) \in B$
16		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
17	2 16	grpinvcl	$⊢ (R \in Grp \land f (x) \in B) \to {inv}_{g} (R) (f (x)) \in B$
18	8 15 17	syl2an	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to {inv}_{g} (R) (f (x)) \in B$
19	5 18	eqeltrid	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to Y \in B$

Metamath Proof Explorer