Metamath Proof Explorer


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 df-ss ( 𝐶 ⊆ ( 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 ( 𝜑𝐵 = ( 𝐶𝐾 ) )