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

Metamath Proof Explorer

Theorem mhmcopsr

Description: The composition of a monoid homomorphism and a power series is a power series. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses mhmcopsr.p ⊢ P = I mPwSer R
mhmcopsr.q ⊢ Q = I mPwSer S
mhmcopsr.b ⊢ B = Base P
mhmcopsr.c ⊢ C = Base Q
mhmcopsr.h ⊢ φ → H ∈ R MndHom S
mhmcopsr.f ⊢ φ → F ∈ B
Assertion mhmcopsr ⊢ φ → H ∘ F ∈ C

Proof

Step Hyp Ref Expression
1 mhmcopsr.p ⊢ P = I mPwSer R
2 mhmcopsr.q ⊢ Q = I mPwSer S
3 mhmcopsr.b ⊢ B = Base P
4 mhmcopsr.c ⊢ C = Base Q
5 mhmcopsr.h ⊢ φ → H ∈ R MndHom S
6 mhmcopsr.f ⊢ φ → F ∈ B
7 fvexd ⊢ φ → Base S ∈ V
8 ovex ⊢ ℕ 0 I ∈ V
9 8 rabex ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∈ V
10 9 a1i ⊢ φ → f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∈ V
11 eqid ⊢ Base R = Base R
12 eqid ⊢ Base S = Base S
13 11 12 mhmf ⊢ H ∈ R MndHom S → H : Base R ⟶ Base S
14 5 13 syl ⊢ φ → H : Base R ⟶ Base S
15 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
16 1 11 15 3 6 psrelbas ⊢ φ → F : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
17 14 16 fcod ⊢ φ → H ∘ F : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base S
18 7 10 17 elmapdd ⊢ φ → H ∘ F ∈ Base S f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
19 reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer
20 19 1 3 elbasov ⊢ F ∈ B → I ∈ V ∧ R ∈ V
21 6 20 syl ⊢ φ → I ∈ V ∧ R ∈ V
22 21 simpld ⊢ φ → I ∈ V
23 2 12 15 4 22 psrbas ⊢ φ → C = Base S f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
24 18 23 eleqtrrd ⊢ φ → H ∘ F ∈ C