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	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
	mhmcopsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
	mhmcopsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mhmcopsr.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	mhmcopsr.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
	mhmcopsr.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	mhmcopsr	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mhmcopsr.p	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
2		mhmcopsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
3		mhmcopsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mhmcopsr.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
5		mhmcopsr.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
6		mhmcopsr.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) ∈ V )
8		ovex	⊢ ( ℕ₀ ↑_m 𝐼 ) ∈ V
9	8	rabex	⊢ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
10	9	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13	11 12	mhmf	⊢ ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
14	5 13	syl	⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
15		eqid	⊢ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin }
16	1 11 15 3 6	psrelbas	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
17	14 16	fcod	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑆 ) )
18	7 10 17	elmapdd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Base ‘ 𝑆 ) ↑_m { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ) )
19		reldmpsr	⊢ Rel dom mPwSer
20	19 1 3	elbasov	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
21	6 20	syl	⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
22	21	simpld	⊢ ( 𝜑 → 𝐼 ∈ V )
23	2 12 15 4 22	psrbas	⊢ ( 𝜑 → 𝐶 = ( ( Base ‘ 𝑆 ) ↑_m { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ) )
24	18 23	eleqtrrd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )

Metamath Proof Explorer

Theorem mhmcopsr

Proof