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	syl5eq	⊢ ( 𝜑 → 𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin } )