Theorem ressmplbas2

Description: The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	ressmpl.s	⊢ 𝑆 = ( 𝐼 mPoly 𝑅 )
	ressmpl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	ressmpl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
	ressmpl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressmpl.1	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	ressmpl.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressmplbas2.w	⊢ 𝑊 = ( 𝐼 mPwSer 𝐻 )
	ressmplbas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
	ressmplbas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion	ressmplbas2	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		ressmpl.s	⊢ 𝑆 = ( 𝐼 mPoly 𝑅 )
2		ressmpl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		ressmpl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
4		ressmpl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressmpl.1	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		ressmpl.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7		ressmplbas2.w	⊢ 𝑊 = ( 𝐼 mPwSer 𝐻 )
8		ressmplbas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
9		ressmplbas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
10		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
11	10 2 7 8	subrgpsr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐶 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
12	5 6 11	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
13		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
14	13	subrgss	⊢ ( 𝐶 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → 𝐶 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
15	12 14	syl	⊢ ( 𝜑 → 𝐶 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
16		dfss2	⊢ ( 𝐶 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↔ ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝐶 )
17	15 16	sylib	⊢ ( 𝜑 → ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝐶 )
18		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19	2 18	subrg0	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
20	6 19	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
21	20	breq2d	⊢ ( 𝜑 → ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ↔ 𝑓 finSupp ( 0g ‘ 𝐻 ) ) )
22	21	abbidv	⊢ ( 𝜑 → { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } = { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } )
23	17 22	ineq12d	⊢ ( 𝜑 → ( ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } ) = ( 𝐶 ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } ) )
24	23	eqcomd	⊢ ( 𝜑 → ( 𝐶 ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } ) = ( ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } ) )
25		eqid	⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
26	3 7 8 25 4	mplbas	⊢ 𝐵 = { 𝑓 ∈ 𝐶 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) }
27		dfrab3	⊢ { 𝑓 ∈ 𝐶 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } = ( 𝐶 ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } )
28	26 27	eqtri	⊢ 𝐵 = ( 𝐶 ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝐻 ) } )
29	1 10 13 18 9	mplbas	⊢ 𝐾 = { 𝑓 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) }
30		dfrab3	⊢ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } = ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } )
31	29 30	eqtri	⊢ 𝐾 = ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } )
32	31	ineq2i	⊢ ( 𝐶 ∩ 𝐾 ) = ( 𝐶 ∩ ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } ) )
33		inass	⊢ ( ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } ) = ( 𝐶 ∩ ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } ) )
34	32 33	eqtr4i	⊢ ( 𝐶 ∩ 𝐾 ) = ( ( 𝐶 ∩ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∩ { 𝑓 ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) } )
35	24 28 34	3eqtr4g	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )