Metamath Proof Explorer


Theorem mplsubglem2

Description: Lemma for mplsubg and mpllss . (Contributed by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubg.s S = I mPwSer R
mplsubg.p P = I mPoly R
mplsubg.u U = Base P
mplsubg.i φ I W
Assertion mplsubglem2 φ U = g Base S | g supp 0 R Fin

Proof

Step Hyp Ref Expression
1 mplsubg.s S = I mPwSer R
2 mplsubg.p P = I mPoly R
3 mplsubg.u U = Base P
4 mplsubg.i φ I W
5 eqid Base S = Base S
6 eqid 0 R = 0 R
7 2 1 5 6 3 mplbas U = g Base S | finSupp 0 R g
8 1 5 psrelbasfun g Base S Fun g
9 8 adantl φ g Base S Fun g
10 simpr φ g Base S g Base S
11 fvexd φ g Base S 0 R V
12 funisfsupp Fun g g Base S 0 R V finSupp 0 R g g supp 0 R Fin
13 9 10 11 12 syl3anc φ g Base S finSupp 0 R g g supp 0 R Fin
14 13 rabbidva φ g Base S | finSupp 0 R g = g Base S | g supp 0 R Fin
15 7 14 syl5eq φ U = g Base S | g supp 0 R Fin