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