Theorem mulcncfOLD

Description: Obsolete version of mulcncf as of 9-Apr-2025. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mulcncfOLD.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
	mulcncfOLD.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion	mulcncfOLD	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		mulcncfOLD.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
2		mulcncfOLD.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
3		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4	3	mulcn	⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
5	4	a1i	⊢ ( 𝜑 → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
6	3 5 1 2	cncfmpt2f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )