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

Metamath Proof Explorer

Theorem psraddcl

Description: Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014) Generalize to magmas. (Revised by SN, 12-Apr-2025)

Ref Expression
Hypotheses psraddcl.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psraddcl.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psraddcl.p ⊢ + = ( +g ‘ 𝑆 )
psraddcl.r ⊢ ( 𝜑 → 𝑅 ∈ Mgm )
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 ⊢ ( 𝜑 → 𝑅 ∈ Mgm )
5 psraddcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 psraddcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 7 8 mgmcl ⊢ ( ( 𝑅 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
10 9 3expb ⊢ ( ( 𝑅 ∈ Mgm ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
11 4 10 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
12 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
13 1 7 12 2 5 psrelbas ⊢ ( 𝜑 → 𝑋 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
14 1 7 12 2 6 psrelbas ⊢ ( 𝜑 → 𝑌 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
15 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
16 15 rabex ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
17 16 a1i ⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
18 inidm ⊢ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∩ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
19 11 13 14 17 17 18 off ⊢ ( 𝜑 → ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
21 20 16 elmap ⊢ ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
22 19 21 sylibr ⊢ ( 𝜑 → ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
29 22 23 28 3eltr4d ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )