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 
|- ( ph -> I e. W )
Assertion mplsubglem2 
|- ( ph -> U = { g e. ( Base ` S ) | ( g supp ( 0g ` R ) ) e. 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 
 |-  ( ph -> I e. W )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 2 1 5 6 3 mplbas 
 |-  U = { g e. ( Base ` S ) | g finSupp ( 0g ` R ) }
8 1 5 psrelbasfun 
 |-  ( g e. ( Base ` S ) -> Fun g )
9 8 adantl 
 |-  ( ( ph /\ g e. ( Base ` S ) ) -> Fun g )
10 simpr 
 |-  ( ( ph /\ g e. ( Base ` S ) ) -> g e. ( Base ` S ) )
11 fvexd 
 |-  ( ( ph /\ g e. ( Base ` S ) ) -> ( 0g ` R ) e. _V )
12 funisfsupp 
 |-  ( ( Fun g /\ g e. ( Base ` S ) /\ ( 0g ` R ) e. _V ) -> ( g finSupp ( 0g ` R ) <-> ( g supp ( 0g ` R ) ) e. Fin ) )
13 9 10 11 12 syl3anc 
 |-  ( ( ph /\ g e. ( Base ` S ) ) -> ( g finSupp ( 0g ` R ) <-> ( g supp ( 0g ` R ) ) e. Fin ) )
14 13 rabbidva 
 |-  ( ph -> { g e. ( Base ` S ) | g finSupp ( 0g ` R ) } = { g e. ( Base ` S ) | ( g supp ( 0g ` R ) ) e. Fin } )
15 7 14 syl5eq 
 |-  ( ph -> U = { g e. ( Base ` S ) | ( g supp ( 0g ` R ) ) e. Fin } )