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

Metamath Proof Explorer

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 ‘ 𝑆 ) )