Theorem subrgpsr

Description: A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	subrgpsr.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	subrgpsr.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgpsr.u	⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
	subrgpsr.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
Assertion	subrgpsr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgpsr.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		subrgpsr.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		subrgpsr.u	⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
4		subrgpsr.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐼 ∈ 𝑉 )
6		subrgrcl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
7	6	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
8	1 5 7	psrring	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ Ring )
9	2	subrgring	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐻 ∈ Ring )
10	9	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐻 ∈ Ring )
11	3 5 10	psrring	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑈 ∈ Ring )
12	4	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 = ( Base ‘ 𝑈 ) )
13		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
14		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
15	1 2 3 4 13 14	resspsrbas	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 = ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
16	1 2 3 4 13 14	resspsradd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑦 ) )
17	1 2 3 4 13 14	resspsrmul	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑈 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑦 ) )
18	12 15 16 17	ringpropd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑈 ∈ Ring ↔ ( 𝑆 ↾s 𝐵 ) ∈ Ring ) )
19	11 18	mpbid	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
20		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21	13 20	ressbasss	⊢ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ⊆ ( Base ‘ 𝑆 )
22	15 21	eqsstrdi	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
23		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
24		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
25		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
27	1 5 7 23 24 25 26	psr1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
28	25	subrg1cl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑇 )
29		subrgsubg	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
30	24	subg0cl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑇 )
31	29 30	syl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑇 )
32	28 31	ifcld	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝑇 )
33	32	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝑇 )
34	2	subrgbas	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
35	34	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑇 = ( Base ‘ 𝐻 ) )
36	33 35	eleqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐻 ) )
37	36	adantr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐻 ) )
38	27 37	fmpt3d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
39		fvex	⊢ ( Base ‘ 𝐻 ) ∈ V
40		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
41	40	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
42	39 41	elmap	⊢ ( ( 1r ‘ 𝑆 ) ∈ ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( 1r ‘ 𝑆 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
43	38 42	sylibr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) ∈ ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
44		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
45	3 44 23 4 5	psrbas	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 = ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
46	43 45	eleqtrrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) ∈ 𝐵 )
47	22 46	jca	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐵 ⊆ ( Base ‘ 𝑆 ) ∧ ( 1r ‘ 𝑆 ) ∈ 𝐵 ) )
48	20 26	issubrg	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) ↔ ( ( 𝑆 ∈ Ring ∧ ( 𝑆 ↾s 𝐵 ) ∈ Ring ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑆 ) ∧ ( 1r ‘ 𝑆 ) ∈ 𝐵 ) ) )
49	8 19 47 48	syl21anbrc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )