Metamath Proof Explorer


Theorem psraddcl

Description: Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psraddcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
psraddcl.b 𝐵 = ( Base ‘ 𝑆 )
psraddcl.p + = ( +g𝑆 )
psraddcl.r ( 𝜑𝑅 ∈ Grp )
psraddcl.x ( 𝜑𝑋𝐵 )
psraddcl.y ( 𝜑𝑌𝐵 )
Assertion psraddcl ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psraddcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psraddcl.b 𝐵 = ( Base ‘ 𝑆 )
3 psraddcl.p + = ( +g𝑆 )
4 psraddcl.r ( 𝜑𝑅 ∈ Grp )
5 psraddcl.x ( 𝜑𝑋𝐵 )
6 psraddcl.y ( 𝜑𝑌𝐵 )
7 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ( +g𝑅 ) = ( +g𝑅 )
9 7 8 grpcl ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
10 9 3expb ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
11 4 10 sylan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
12 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
13 1 7 12 2 5 psrelbas ( 𝜑𝑋 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
14 1 7 12 2 6 psrelbas ( 𝜑𝑌 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
15 ovex ( ℕ0m 𝐼 ) ∈ V
16 15 rabex { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V
17 16 a1i ( 𝜑 → { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V )
18 inidm ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
19 11 13 14 17 17 18 off ( 𝜑 → ( 𝑋f ( +g𝑅 ) 𝑌 ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20 fvex ( Base ‘ 𝑅 ) ∈ V
21 20 16 elmap ( ( 𝑋f ( +g𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( 𝑋f ( +g𝑅 ) 𝑌 ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
22 19 21 sylibr ( 𝜑 → ( 𝑋f ( +g𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
23 1 2 8 3 5 6 psradd ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋f ( +g𝑅 ) 𝑌 ) )
24 reldmpsr Rel dom mPwSer
25 24 1 2 elbasov ( 𝑋𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
26 5 25 syl ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
27 26 simpld ( 𝜑𝐼 ∈ V )
28 1 7 12 2 27 psrbas ( 𝜑𝐵 = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
29 22 23 28 3eltr4d ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )