Theorem fmulcl

Description: If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fmulcl.1	⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
	fmulcl.2	⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
	fmulcl.4	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑀 ) )
	fmulcl.5	⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
	fmulcl.6	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
	fmulcl.7	⊢ ( 𝜑 → 𝑇 ∈ V )
Assertion	fmulcl	⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		fmulcl.1	⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
2		fmulcl.2	⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 )
3		fmulcl.4	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑀 ) )
4		fmulcl.5	⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
5		fmulcl.6	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
6		fmulcl.7	⊢ ( 𝜑 → 𝑇 ∈ V )
7		elfzuz	⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
8	3 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
9		elfzuz3	⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
10		fzss2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) )
11	3 9 10	3syl	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) )
12	11	sselda	⊢ ( ( 𝜑 ∧ ℎ ∈ ( 1 ... 𝑁 ) ) → ℎ ∈ ( 1 ... 𝑀 ) )
13	4	ffvelrnda	⊢ ( ( 𝜑 ∧ ℎ ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ ℎ ) ∈ 𝑌 )
14	12 13	syldan	⊢ ( ( 𝜑 ∧ ℎ ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ ℎ ) ∈ 𝑌 )
15		simprl	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → ℎ ∈ 𝑌 )
16		simprr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → 𝑙 ∈ 𝑌 )
17	6	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → 𝑇 ∈ V )
18		mptexg	⊢ ( 𝑇 ∈ V → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ V )
19	17 18	syl	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ V )
20		fveq1	⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 𝑡 ) = ( ℎ ‘ 𝑡 ) )
21		fveq1	⊢ ( 𝑔 = 𝑙 → ( 𝑔 ‘ 𝑡 ) = ( 𝑙 ‘ 𝑡 ) )
22	20 21	oveqan12d	⊢ ( ( 𝑓 = ℎ ∧ 𝑔 = 𝑙 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
23	22	mpteq2dv	⊢ ( ( 𝑓 = ℎ ∧ 𝑔 = 𝑙 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
24	23 1	ovmpoga	⊢ ( ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ V ) → ( ℎ 𝑃 𝑙 ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
25	15 16 19 24	syl3anc	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → ( ℎ 𝑃 𝑙 ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
26		3simpc	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) )
27		eleq1w	⊢ ( 𝑓 = ℎ → ( 𝑓 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
28	27	3anbi2d	⊢ ( 𝑓 = ℎ → ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ) )
29	20	oveq1d	⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
30	29	mpteq2dv	⊢ ( 𝑓 = ℎ → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
31	30	eleq1d	⊢ ( 𝑓 = ℎ → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
32	28 31	imbi12d	⊢ ( 𝑓 = ℎ → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ) )
33		eleq1w	⊢ ( 𝑔 = 𝑙 → ( 𝑔 ∈ 𝑌 ↔ 𝑙 ∈ 𝑌 ) )
34	33	3anbi3d	⊢ ( 𝑔 = 𝑙 → ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) )
35	21	oveq2d	⊢ ( 𝑔 = 𝑙 → ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) )
36	35	mpteq2dv	⊢ ( 𝑔 = 𝑙 → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) )
37	36	eleq1d	⊢ ( 𝑔 = 𝑙 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
38	34 37	imbi12d	⊢ ( 𝑔 = 𝑙 → ( ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) ) )
39	32 38 5	vtocl2g	⊢ ( ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 ) )
40	26 39	mpcom	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 )
41	40	3expb	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) · ( 𝑙 ‘ 𝑡 ) ) ) ∈ 𝑌 )
42	25 41	eqeltrd	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝑌 ∧ 𝑙 ∈ 𝑌 ) ) → ( ℎ 𝑃 𝑙 ) ∈ 𝑌 )
43	8 14 42	seqcl	⊢ ( 𝜑 → ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑁 ) ∈ 𝑌 )
44	2 43	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )