Metamath Proof Explorer


Theorem 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=BaseM
lincext.r R=ScalarM
lincext.e E=BaseR
lincext.0 0˙=0R
lincext.z Z=0M
lincext.n N=invgR
lincext.f F=zSifz=XNYGz
Assertion lincext2 MLModS𝒫BYEXSGESXfinSupp0˙GfinSupp0˙F

Proof

Step Hyp Ref Expression
1 lincext.b B=BaseM
2 lincext.r R=ScalarM
3 lincext.e E=BaseR
4 lincext.0 0˙=0R
5 lincext.z Z=0M
6 lincext.n N=invgR
7 lincext.f F=zSifz=XNYGz
8 fvex NYV
9 fvex GzV
10 8 9 ifex ifz=XNYGzV
11 10 7 dmmpti domF=S
12 11 difeq1i domFSX=SSX
13 snssi XSXS
14 13 3ad2ant2 YEXSGESXXS
15 14 3ad2ant2 MLModS𝒫BYEXSGESXfinSupp0˙GXS
16 dfss4 XSSSX=X
17 15 16 sylib MLModS𝒫BYEXSGESXfinSupp0˙GSSX=X
18 snfi XFin
19 17 18 eqeltrdi MLModS𝒫BYEXSGESXfinSupp0˙GSSXFin
20 12 19 eqeltrid MLModS𝒫BYEXSGESXfinSupp0˙GdomFSXFin
21 1 2 3 4 5 6 7 lincext1 MLModS𝒫BYEXSGESXFES
22 21 3adant3 MLModS𝒫BYEXSGESXfinSupp0˙GFES
23 elmapfun FESFunF
24 22 23 syl MLModS𝒫BYEXSGESXfinSupp0˙GFunF
25 elmapi GESXG:SXE
26 7 fdmdifeqresdif G:SXEG=FSX
27 25 26 syl GESXG=FSX
28 27 3ad2ant3 YEXSGESXG=FSX
29 28 3ad2ant2 MLModS𝒫BYEXSGESXfinSupp0˙GG=FSX
30 simp3 MLModS𝒫BYEXSGESXfinSupp0˙GfinSupp0˙G
31 4 fvexi 0˙V
32 31 a1i MLModS𝒫BYEXSGESXfinSupp0˙G0˙V
33 20 22 24 29 30 32 resfsupp MLModS𝒫BYEXSGESXfinSupp0˙GfinSupp0˙F