This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplsubglem2

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

Ref Expression
Hypotheses mplsubg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubg.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplsubg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
mplsubg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
Assertion mplsubglem2 ( 𝜑 → 𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin } )

Proof

Step Hyp Ref Expression
1 mplsubg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubg.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mplsubg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 mplsubg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 2 1 5 6 3 mplbas ⊢ 𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ 𝑔 finSupp ( 0g ‘ 𝑅 ) }
8 1 5 psrelbasfun ⊢ ( 𝑔 ∈ ( Base ‘ 𝑆 ) → Fun 𝑔 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → Fun 𝑔 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → 𝑔 ∈ ( Base ‘ 𝑆 ) )
11 fvexd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
12 funisfsupp ⊢ ( ( Fun 𝑔 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) → ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ↔ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ) )
13 9 10 11 12 syl3anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 finSupp ( 0g ‘ 𝑅 ) ↔ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ) )
14 13 rabbidva ⊢ ( 𝜑 → { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ 𝑔 finSupp ( 0g ‘ 𝑅 ) } = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin } )
15 7 14 eqtrid ⊢ ( 𝜑 → 𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin } )