Metamath Proof Explorer


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
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
fmulcl.2
|- X = ( seq 1 ( P , U ) ` N )
fmulcl.4
|- ( ph -> N e. ( 1 ... M ) )
fmulcl.5
|- ( ph -> U : ( 1 ... M ) --> Y )
fmulcl.6
|- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
fmulcl.7
|- ( ph -> T e. _V )
Assertion fmulcl
|- ( ph -> X e. Y )

Proof

Step Hyp Ref Expression
1 fmulcl.1
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
2 fmulcl.2
 |-  X = ( seq 1 ( P , U ) ` N )
3 fmulcl.4
 |-  ( ph -> N e. ( 1 ... M ) )
4 fmulcl.5
 |-  ( ph -> U : ( 1 ... M ) --> Y )
5 fmulcl.6
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
6 fmulcl.7
 |-  ( ph -> T e. _V )
7 elfzuz
 |-  ( N e. ( 1 ... M ) -> N e. ( ZZ>= ` 1 ) )
8 3 7 syl
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
9 elfzuz3
 |-  ( N e. ( 1 ... M ) -> M e. ( ZZ>= ` N ) )
10 fzss2
 |-  ( M e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... M ) )
11 3 9 10 3syl
 |-  ( ph -> ( 1 ... N ) C_ ( 1 ... M ) )
12 11 sselda
 |-  ( ( ph /\ h e. ( 1 ... N ) ) -> h e. ( 1 ... M ) )
13 4 ffvelrnda
 |-  ( ( ph /\ h e. ( 1 ... M ) ) -> ( U ` h ) e. Y )
14 12 13 syldan
 |-  ( ( ph /\ h e. ( 1 ... N ) ) -> ( U ` h ) e. Y )
15 simprl
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> h e. Y )
16 simprr
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> l e. Y )
17 6 adantr
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> T e. _V )
18 mptexg
 |-  ( T e. _V -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. _V )
19 17 18 syl
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. _V )
20 fveq1
 |-  ( f = h -> ( f ` t ) = ( h ` t ) )
21 fveq1
 |-  ( g = l -> ( g ` t ) = ( l ` t ) )
22 20 21 oveqan12d
 |-  ( ( f = h /\ g = l ) -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
23 22 mpteq2dv
 |-  ( ( f = h /\ g = l ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
24 23 1 ovmpoga
 |-  ( ( h e. Y /\ l e. Y /\ ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. _V ) -> ( h P l ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
25 15 16 19 24 syl3anc
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> ( h P l ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
26 3simpc
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( h e. Y /\ l e. Y ) )
27 eleq1w
 |-  ( f = h -> ( f e. Y <-> h e. Y ) )
28 27 3anbi2d
 |-  ( f = h -> ( ( ph /\ f e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ g e. Y ) ) )
29 20 oveq1d
 |-  ( f = h -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( g ` t ) ) )
30 29 mpteq2dv
 |-  ( f = h -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) )
31 30 eleq1d
 |-  ( f = h -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) )
32 28 31 imbi12d
 |-  ( f = h -> ( ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y ) <-> ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) ) )
33 eleq1w
 |-  ( g = l -> ( g e. Y <-> l e. Y ) )
34 33 3anbi3d
 |-  ( g = l -> ( ( ph /\ h e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ l e. Y ) ) )
35 21 oveq2d
 |-  ( g = l -> ( ( h ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
36 35 mpteq2dv
 |-  ( g = l -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
37 36 eleq1d
 |-  ( g = l -> ( ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
38 34 37 imbi12d
 |-  ( g = l -> ( ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) <-> ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) ) )
39 32 38 5 vtocl2g
 |-  ( ( h e. Y /\ l e. Y ) -> ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
40 26 39 mpcom
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
41 40 3expb
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
42 25 41 eqeltrd
 |-  ( ( ph /\ ( h e. Y /\ l e. Y ) ) -> ( h P l ) e. Y )
43 8 14 42 seqcl
 |-  ( ph -> ( seq 1 ( P , U ) ` N ) e. Y )
44 2 43 eqeltrid
 |-  ( ph -> X e. Y )