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	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
	fmulcl.2	$⊢ X = seq 1 (P, U) (N)$
	fmulcl.4	$⊢ φ \to N \in (1 \dots M)$
	fmulcl.5	$⊢ φ \to U : (1 \dots M) ⟶ Y$
	fmulcl.6	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
	fmulcl.7	$⊢ φ \to T \in V$
Assertion	fmulcl	$⊢ φ \to X \in Y$

Proof

Step	Hyp	Ref	Expression
1		fmulcl.1	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
2		fmulcl.2	$⊢ X = seq 1 (P, U) (N)$
3		fmulcl.4	$⊢ φ \to N \in (1 \dots M)$
4		fmulcl.5	$⊢ φ \to U : (1 \dots M) ⟶ Y$
5		fmulcl.6	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
6		fmulcl.7	$⊢ φ \to T \in V$
7		elfzuz	$⊢ N \in (1 \dots M) \to N \in ℤ_{\geq 1}$
8	3 7	syl	$⊢ φ \to N \in ℤ_{\geq 1}$
9		elfzuz3	$⊢ N \in (1 \dots M) \to M \in ℤ_{\geq N}$
10		fzss2	$⊢ M \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots M)$
11	3 9 10	3syl	$⊢ φ \to (1 \dots N) \subseteq (1 \dots M)$
12	11	sselda	$⊢ (φ \land h \in (1 \dots N)) \to h \in (1 \dots M)$
13	4	ffvelrnda	$⊢ (φ \land h \in (1 \dots M)) \to U (h) \in Y$
14	12 13	syldan	$⊢ (φ \land h \in (1 \dots N)) \to U (h) \in Y$
15		simprl	$⊢ (φ \land (h \in Y \land l \in Y)) \to h \in Y$
16		simprr	$⊢ (φ \land (h \in Y \land l \in Y)) \to l \in Y$
17	6	adantr	$⊢ (φ \land (h \in Y \land l \in Y)) \to T \in V$
18		mptexg	$⊢ T \in V \to (t \in T ⟼ h (t) l (t)) \in V$
19	17 18	syl	$⊢ (φ \land (h \in Y \land l \in Y)) \to (t \in T ⟼ h (t) l (t)) \in V$
20		fveq1	$⊢ f = h \to f (t) = h (t)$
21		fveq1	$⊢ g = l \to g (t) = l (t)$
22	20 21	oveqan12d	$⊢ (f = h \land g = l) \to f (t) g (t) = h (t) l (t)$
23	22	mpteq2dv	$⊢ (f = h \land g = l) \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ h (t) l (t))$
24	23 1	ovmpoga	$⊢ (h \in Y \land l \in Y \land (t \in T ⟼ h (t) l (t)) \in V) \to h P l = (t \in T ⟼ h (t) l (t))$
25	15 16 19 24	syl3anc	$⊢ (φ \land (h \in Y \land l \in Y)) \to h P l = (t \in T ⟼ h (t) l (t))$
26		3simpc	$⊢ (φ \land h \in Y \land l \in Y) \to (h \in Y \land l \in Y)$
27		eleq1w	$⊢ f = h \to (f \in Y \leftrightarrow h \in Y)$
28	27	3anbi2d	$⊢ f = h \to ((φ \land f \in Y \land g \in Y) \leftrightarrow (φ \land h \in Y \land g \in Y))$
29	20	oveq1d	$⊢ f = h \to f (t) g (t) = h (t) g (t)$
30	29	mpteq2dv	$⊢ f = h \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ h (t) g (t))$
31	30	eleq1d	$⊢ f = h \to ((t \in T ⟼ f (t) g (t)) \in Y \leftrightarrow (t \in T ⟼ h (t) g (t)) \in Y)$
32	28 31	imbi12d	$⊢ f = h \to (((φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y) \leftrightarrow ((φ \land h \in Y \land g \in Y) \to (t \in T ⟼ h (t) g (t)) \in Y))$
33		eleq1w	$⊢ g = l \to (g \in Y \leftrightarrow l \in Y)$
34	33	3anbi3d	$⊢ g = l \to ((φ \land h \in Y \land g \in Y) \leftrightarrow (φ \land h \in Y \land l \in Y))$
35	21	oveq2d	$⊢ g = l \to h (t) g (t) = h (t) l (t)$
36	35	mpteq2dv	$⊢ g = l \to (t \in T ⟼ h (t) g (t)) = (t \in T ⟼ h (t) l (t))$
37	36	eleq1d	$⊢ g = l \to ((t \in T ⟼ h (t) g (t)) \in Y \leftrightarrow (t \in T ⟼ h (t) l (t)) \in Y)$
38	34 37	imbi12d	$⊢ g = l \to (((φ \land h \in Y \land g \in Y) \to (t \in T ⟼ h (t) g (t)) \in Y) \leftrightarrow ((φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y))$
39	32 38 5	vtocl2g	$⊢ (h \in Y \land l \in Y) \to ((φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y)$
40	26 39	mpcom	$⊢ (φ \land h \in Y \land l \in Y) \to (t \in T ⟼ h (t) l (t)) \in Y$
41	40	3expb	$⊢ (φ \land (h \in Y \land l \in Y)) \to (t \in T ⟼ h (t) l (t)) \in Y$
42	25 41	eqeltrd	$⊢ (φ \land (h \in Y \land l \in Y)) \to h P l \in Y$
43	8 14 42	seqcl	$⊢ φ \to seq 1 (P, U) (N) \in Y$
44	2 43	eqeltrid	$⊢ φ \to X \in Y$

Metamath Proof Explorer

Theorem fmulcl

Proof