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 ffvelcdmda 
 |-  ( ( 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 )