lindslinindimp2lem2

Description: Lemma 2 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	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\})})$

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		elmapi	$⊢ f \in (B^{S}) \to f : S ⟶ B$
8	7	3ad2ant3	$⊢ (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S})) \to f : S ⟶ B$
9	8	adantl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to f : S ⟶ B$
10		difss	$⊢ S ∖ \{x\} \subseteq S$
11		fssres	$⊢ (f : S ⟶ B \land S ∖ \{x\} \subseteq S) \to ({f ↾}_{(S ∖ \{x\})}) : S ∖ \{x\} ⟶ B$
12	9 10 11	sylancl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to ({f ↾}_{(S ∖ \{x\})}) : S ∖ \{x\} ⟶ B$
13	6	feq1i	$⊢ G : S ∖ \{x\} ⟶ B \leftrightarrow ({f ↾}_{(S ∖ \{x\})}) : S ∖ \{x\} ⟶ B$
14	12 13	sylibr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to G : S ∖ \{x\} ⟶ B$
15	2	fvexi	$⊢ B \in V$
16		difexg	$⊢ S \in V \to S ∖ \{x\} \in V$
17	16	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to S ∖ \{x\} \in V$
18		elmapg	$⊢ (B \in V \land S ∖ \{x\} \in V) \to (G \in (B^{(S ∖ \{x\})}) \leftrightarrow G : S ∖ \{x\} ⟶ B)$
19	15 17 18	sylancr	$⊢ ((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\})}) \leftrightarrow G : S ∖ \{x\} ⟶ B)$
20	14 19	mpbird	$⊢ ((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\})})$

Metamath Proof Explorer

Theorem lindslinindimp2lem2

Proof