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

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 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 ⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )