lincext2

Description: Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	lincext.b	$⊢ B = {Base}_{M}$
	lincext.r	$⊢ R = Scalar (M)$
	lincext.e	$⊢ E = {Base}_{R}$
	lincext.0	$⊢ \underset{˙}{0} = 0_{R}$
	lincext.z	$⊢ Z = 0_{M}$
	lincext.n	$⊢ N = {inv}_{g} (R)$
	lincext.f	$⊢ F = (z \in S ⟼ if (z = X, N (Y), G (z)))$
Assertion	lincext2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to {finSupp}_{\underset{˙}{0}} (F)$

Proof

Step	Hyp	Ref	Expression
1		lincext.b	$⊢ B = {Base}_{M}$
2		lincext.r	$⊢ R = Scalar (M)$
3		lincext.e	$⊢ E = {Base}_{R}$
4		lincext.0	$⊢ \underset{˙}{0} = 0_{R}$
5		lincext.z	$⊢ Z = 0_{M}$
6		lincext.n	$⊢ N = {inv}_{g} (R)$
7		lincext.f	$⊢ F = (z \in S ⟼ if (z = X, N (Y), G (z)))$
8		fvex	$⊢ N (Y) \in V$
9		fvex	$⊢ G (z) \in V$
10	8 9	ifex	$⊢ if (z = X, N (Y), G (z)) \in V$
11	10 7	dmmpti	$⊢ dom F = S$
12	11	difeq1i	$⊢ dom F ∖ (S ∖ \{X\}) = S ∖ (S ∖ \{X\})$
13		snssi	$⊢ X \in S \to \{X\} \subseteq S$
14	13	3ad2ant2	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to \{X\} \subseteq S$
15	14	3ad2ant2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to \{X\} \subseteq S$
16		dfss4	$⊢ \{X\} \subseteq S \leftrightarrow S ∖ (S ∖ \{X\}) = \{X\}$
17	15 16	sylib	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to S ∖ (S ∖ \{X\}) = \{X\}$
18		snfi	$⊢ \{X\} \in Fin$
19	17 18	eqeltrdi	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to S ∖ (S ∖ \{X\}) \in Fin$
20	12 19	eqeltrid	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to dom F ∖ (S ∖ \{X\}) \in Fin$
21	1 2 3 4 5 6 7	lincext1	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to F \in (E^{S})$
22	21	3adant3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to F \in (E^{S})$
23		elmapfun	$⊢ F \in (E^{S}) \to Fun F$
24	22 23	syl	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to Fun F$
25		elmapi	$⊢ G \in (E^{(S ∖ \{X\})}) \to G : S ∖ \{X\} ⟶ E$
26	7	fdmdifeqresdif	$⊢ G : S ∖ \{X\} ⟶ E \to G = {F ↾}_{(S ∖ \{X\})}$
27	25 26	syl	$⊢ G \in (E^{(S ∖ \{X\})}) \to G = {F ↾}_{(S ∖ \{X\})}$
28	27	3ad2ant3	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to G = {F ↾}_{(S ∖ \{X\})}$
29	28	3ad2ant2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to G = {F ↾}_{(S ∖ \{X\})}$
30		simp3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to {finSupp}_{\underset{˙}{0}} (G)$
31	4	fvexi	$⊢ \underset{˙}{0} \in V$
32	31	a1i	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to \underset{˙}{0} \in V$
33	20 22 24 29 30 32	resfsupp	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to {finSupp}_{\underset{˙}{0}} (F)$

Metamath Proof Explorer

Theorem lincext2

Proof