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 eqtrid ⊢ φ → U = g ∈ Base S | g supp 0 R ∈ Fin