Metamath Proof Explorer

Theorem fmuldfeq

Description: X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmuldfeq.1 
|- F/ i ph
fmuldfeq.2 
|- F/_ t Y
fmuldfeq.3 
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
fmuldfeq.4 
|- X = ( seq 1 ( P , U ) ` M )
fmuldfeq.5 
|- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
fmuldfeq.6 
|- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
fmuldfeq.7 
|- ( ph -> T e. _V )
fmuldfeq.8 
|- ( ph -> M e. NN )
fmuldfeq.9 
|- ( ph -> U : ( 1 ... M ) --> Y )
fmuldfeq.10 
|- ( ( ph /\ f e. Y ) -> f : T --> RR )
fmuldfeq.11 
|- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
Assertion fmuldfeq 
|- ( ( ph /\ t e. T ) -> ( X ` t ) = ( Z ` t ) )

Proof

Step Hyp Ref Expression
1 fmuldfeq.1 
 |-  F/ i ph
2 fmuldfeq.2 
 |-  F/_ t Y
3 fmuldfeq.3 
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
4 fmuldfeq.4 
 |-  X = ( seq 1 ( P , U ) ` M )
5 fmuldfeq.5 
 |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
6 fmuldfeq.6 
 |-  Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
7 fmuldfeq.7 
 |-  ( ph -> T e. _V )
8 fmuldfeq.8 
 |-  ( ph -> M e. NN )
9 fmuldfeq.9 
 |-  ( ph -> U : ( 1 ... M ) --> Y )
10 fmuldfeq.10 
 |-  ( ( ph /\ f e. Y ) -> f : T --> RR )
11 fmuldfeq.11 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
12 1zzd 
 |-  ( ( ph /\ t e. T ) -> 1 e. ZZ )
13 8 nnzd 
 |-  ( ph -> M e. ZZ )
14 13 adantr 
 |-  ( ( ph /\ t e. T ) -> M e. ZZ )
15 8 nnge1d 
 |-  ( ph -> 1 <_ M )
16 15 adantr 
 |-  ( ( ph /\ t e. T ) -> 1 <_ M )
17 nnre 
 |-  ( M e. NN -> M e. RR )
18 leid 
 |-  ( M e. RR -> M <_ M )
19 8 17 18 3syl 
 |-  ( ph -> M <_ M )
20 19 adantr 
 |-  ( ( ph /\ t e. T ) -> M <_ M )
21 12 14 14 16 20 elfzd 
 |-  ( ( ph /\ t e. T ) -> M e. ( 1 ... M ) )
22 8 3ad2ant1 
 |-  ( ( ph /\ t e. T /\ M e. ( 1 ... M ) ) -> M e. NN )
23 eleq1 
 |-  ( m = 1 -> ( m e. ( 1 ... M ) <-> 1 e. ( 1 ... M ) ) )
24 23 3anbi3d 
 |-  ( m = 1 -> ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) <-> ( ph /\ t e. T /\ 1 e. ( 1 ... M ) ) ) )
25 fveq2 
 |-  ( m = 1 -> ( seq 1 ( P , U ) ` m ) = ( seq 1 ( P , U ) ` 1 ) )
26 25 fveq1d 
 |-  ( m = 1 -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( ( seq 1 ( P , U ) ` 1 ) ` t ) )
27 fveq2 
 |-  ( m = 1 -> ( seq 1 ( x. , ( F ` t ) ) ` m ) = ( seq 1 ( x. , ( F ` t ) ) ` 1 ) )
28 26 27 eqeq12d 
 |-  ( m = 1 -> ( ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) <-> ( ( seq 1 ( P , U ) ` 1 ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` 1 ) ) )
29 24 28 imbi12d 
 |-  ( m = 1 -> ( ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) ) <-> ( ( ph /\ t e. T /\ 1 e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` 1 ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` 1 ) ) ) )
30 eleq1 
 |-  ( m = n -> ( m e. ( 1 ... M ) <-> n e. ( 1 ... M ) ) )
31 30 3anbi3d 
 |-  ( m = n -> ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) <-> ( ph /\ t e. T /\ n e. ( 1 ... M ) ) ) )
32 fveq2 
 |-  ( m = n -> ( seq 1 ( P , U ) ` m ) = ( seq 1 ( P , U ) ` n ) )
33 32 fveq1d 
 |-  ( m = n -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( ( seq 1 ( P , U ) ` n ) ` t ) )
34 fveq2 
 |-  ( m = n -> ( seq 1 ( x. , ( F ` t ) ) ` m ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) )
35 33 34 eqeq12d 
 |-  ( m = n -> ( ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) <-> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) )
36 31 35 imbi12d 
 |-  ( m = n -> ( ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) ) <-> ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) )
37 eleq1 
 |-  ( m = ( n + 1 ) -> ( m e. ( 1 ... M ) <-> ( n + 1 ) e. ( 1 ... M ) ) )
38 37 3anbi3d 
 |-  ( m = ( n + 1 ) -> ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) <-> ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) )
39 fveq2 
 |-  ( m = ( n + 1 ) -> ( seq 1 ( P , U ) ` m ) = ( seq 1 ( P , U ) ` ( n + 1 ) ) )
40 39 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) )
41 fveq2 
 |-  ( m = ( n + 1 ) -> ( seq 1 ( x. , ( F ` t ) ) ` m ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) )
42 40 41 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) <-> ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) ) )
43 38 42 imbi12d 
 |-  ( m = ( n + 1 ) -> ( ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) ) <-> ( ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) ) ) )
44 eleq1 
 |-  ( m = M -> ( m e. ( 1 ... M ) <-> M e. ( 1 ... M ) ) )
45 44 3anbi3d 
 |-  ( m = M -> ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) <-> ( ph /\ t e. T /\ M e. ( 1 ... M ) ) ) )
46 fveq2 
 |-  ( m = M -> ( seq 1 ( P , U ) ` m ) = ( seq 1 ( P , U ) ` M ) )
47 46 fveq1d 
 |-  ( m = M -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( ( seq 1 ( P , U ) ` M ) ` t ) )
48 fveq2 
 |-  ( m = M -> ( seq 1 ( x. , ( F ` t ) ) ` m ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
49 47 48 eqeq12d 
 |-  ( m = M -> ( ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) <-> ( ( seq 1 ( P , U ) ` M ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) ) )
50 45 49 imbi12d 
 |-  ( m = M -> ( ( ( ph /\ t e. T /\ m e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` m ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` m ) ) <-> ( ( ph /\ t e. T /\ M e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` M ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) ) ) )
51 1z 
 |-  1 e. ZZ
52 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( x. , ( F ` t ) ) ` 1 ) = ( ( F ` t ) ` 1 ) )
53 51 52 ax-mp 
 |-  ( seq 1 ( x. , ( F ` t ) ) ` 1 ) = ( ( F ` t ) ` 1 )
54 1zzd 
 |-  ( ph -> 1 e. ZZ )
55 1le1 
 |-  1 <_ 1
56 55 a1i 
 |-  ( ph -> 1 <_ 1 )
57 54 13 54 56 15 elfzd 
 |-  ( ph -> 1 e. ( 1 ... M ) )
58 nfv 
 |-  F/ i t e. T
59 nfcv 
 |-  F/_ i T
60 nfmpt1 
 |-  F/_ i ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )
61 59 60 nfmpt 
 |-  F/_ i ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
62 5 61 nfcxfr 
 |-  F/_ i F
63 nfcv 
 |-  F/_ i t
64 62 63 nffv 
 |-  F/_ i ( F ` t )
65 nfcv 
 |-  F/_ i 1
66 64 65 nffv 
 |-  F/_ i ( ( F ` t ) ` 1 )
67 nffvmpt1 
 |-  F/_ i ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 )
68 66 67 nfeq 
 |-  F/ i ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 )
69 58 68 nfim 
 |-  F/ i ( t e. T -> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) )
70 fveq2 
 |-  ( i = 1 -> ( ( F ` t ) ` i ) = ( ( F ` t ) ` 1 ) )
71 fveq2 
 |-  ( i = 1 -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) )
72 70 71 eqeq12d 
 |-  ( i = 1 -> ( ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) <-> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) ) )
73 72 imbi2d 
 |-  ( i = 1 -> ( ( t e. T -> ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) ) <-> ( t e. T -> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) ) ) )
74 ovex 
 |-  ( 1 ... M ) e. _V
75 74 mptex 
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V
76 5 fvmpt2 
 |-  ( ( t e. T /\ ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
77 75 76 mpan2 
 |-  ( t e. T -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
78 77 fveq1d 
 |-  ( t e. T -> ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) )
79 69 73 78 vtoclg1f 
 |-  ( 1 e. ( 1 ... M ) -> ( t e. T -> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) ) )
80 57 79 syl 
 |-  ( ph -> ( t e. T -> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) ) )
81 80 imp 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` 1 ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) )
82 eqid 
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )
83 fveq2 
 |-  ( i = 1 -> ( U ` i ) = ( U ` 1 ) )
84 83 fveq1d 
 |-  ( i = 1 -> ( ( U ` i ) ` t ) = ( ( U ` 1 ) ` t ) )
85 57 adantr 
 |-  ( ( ph /\ t e. T ) -> 1 e. ( 1 ... M ) )
86 9 57 ffvelrnd 
 |-  ( ph -> ( U ` 1 ) e. Y )
87 86 ancli 
 |-  ( ph -> ( ph /\ ( U ` 1 ) e. Y ) )
88 eleq1 
 |-  ( f = ( U ` 1 ) -> ( f e. Y <-> ( U ` 1 ) e. Y ) )
89 88 anbi2d 
 |-  ( f = ( U ` 1 ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( U ` 1 ) e. Y ) ) )
90 feq1 
 |-  ( f = ( U ` 1 ) -> ( f : T --> RR <-> ( U ` 1 ) : T --> RR ) )
91 89 90 imbi12d 
 |-  ( f = ( U ` 1 ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` 1 ) e. Y ) -> ( U ` 1 ) : T --> RR ) ) )
92 10 a1i 
 |-  ( f e. Y -> ( ( ph /\ f e. Y ) -> f : T --> RR ) )
93 91 92 vtoclga 
 |-  ( ( U ` 1 ) e. Y -> ( ( ph /\ ( U ` 1 ) e. Y ) -> ( U ` 1 ) : T --> RR ) )
94 86 87 93 sylc 
 |-  ( ph -> ( U ` 1 ) : T --> RR )
95 94 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( ( U ` 1 ) ` t ) e. RR )
96 82 84 85 95 fvmptd3 
 |-  ( ( ph /\ t e. T ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` 1 ) = ( ( U ` 1 ) ` t ) )
97 81 96 eqtrd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` 1 ) = ( ( U ` 1 ) ` t ) )
98 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( P , U ) ` 1 ) = ( U ` 1 ) )
99 51 98 ax-mp 
 |-  ( seq 1 ( P , U ) ` 1 ) = ( U ` 1 )
100 99 fveq1i 
 |-  ( ( seq 1 ( P , U ) ` 1 ) ` t ) = ( ( U ` 1 ) ` t )
101 97 100 eqtr4di 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` 1 ) = ( ( seq 1 ( P , U ) ` 1 ) ` t ) )
102 53 101 eqtr2id 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` 1 ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` 1 ) )
103 102 3adant3 
 |-  ( ( ph /\ t e. T /\ 1 e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` 1 ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` 1 ) )
104 simp31 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ph )
105 simp1 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> n e. NN )
106 simp33 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( n + 1 ) e. ( 1 ... M ) )
107 105 106 jca 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... M ) ) )
108 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
109 108 biimpi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
110 109 anim1i 
 |-  ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... M ) ) -> ( n e. ( ZZ>= ` 1 ) /\ ( n + 1 ) e. ( 1 ... M ) ) )
111 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` 1 ) /\ ( n + 1 ) e. ( 1 ... M ) ) -> n e. ( 1 ... M ) )
112 107 110 111 3syl 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> n e. ( 1 ... M ) )
113 simp32 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> t e. T )
114 simp2 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) )
115 104 113 112 114 mp3and 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) )
116 112 106 115 3jca 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) )
117 nfv 
 |-  F/ f ph
118 nfv 
 |-  F/ f n e. ( 1 ... M )
119 nfv 
 |-  F/ f ( n + 1 ) e. ( 1 ... M )
120 nfcv 
 |-  F/_ f 1
121 nfmpo1 
 |-  F/_ f ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
122 3 121 nfcxfr 
 |-  F/_ f P
123 nfcv 
 |-  F/_ f U
124 120 122 123 nfseq 
 |-  F/_ f seq 1 ( P , U )
125 nfcv 
 |-  F/_ f n
126 124 125 nffv 
 |-  F/_ f ( seq 1 ( P , U ) ` n )
127 nfcv 
 |-  F/_ f t
128 126 127 nffv 
 |-  F/_ f ( ( seq 1 ( P , U ) ` n ) ` t )
129 nfcv 
 |-  F/_ f ( seq 1 ( x. , ( F ` t ) ) ` n )
130 128 129 nfeq 
 |-  F/ f ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n )
131 118 119 130 nf3an 
 |-  F/ f ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) )
132 117 131 nfan 
 |-  F/ f ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) )
133 nfv 
 |-  F/ g ph
134 nfv 
 |-  F/ g n e. ( 1 ... M )
135 nfv 
 |-  F/ g ( n + 1 ) e. ( 1 ... M )
136 nfcv 
 |-  F/_ g 1
137 nfmpo2 
 |-  F/_ g ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
138 3 137 nfcxfr 
 |-  F/_ g P
139 nfcv 
 |-  F/_ g U
140 136 138 139 nfseq 
 |-  F/_ g seq 1 ( P , U )
141 nfcv 
 |-  F/_ g n
142 140 141 nffv 
 |-  F/_ g ( seq 1 ( P , U ) ` n )
143 nfcv 
 |-  F/_ g t
144 142 143 nffv 
 |-  F/_ g ( ( seq 1 ( P , U ) ` n ) ` t )
145 nfcv 
 |-  F/_ g ( seq 1 ( x. , ( F ` t ) ) ` n )
146 144 145 nfeq 
 |-  F/ g ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n )
147 134 135 146 nf3an 
 |-  F/ g ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) )
148 133 147 nfan 
 |-  F/ g ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) )
149 7 adantr 
 |-  ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) -> T e. _V )
150 9 adantr 
 |-  ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) -> U : ( 1 ... M ) --> Y )
151 11 3adant1r 
 |-  ( ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
152 simpr1 
 |-  ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) -> n e. ( 1 ... M ) )
153 simpr2 
 |-  ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) -> ( n + 1 ) e. ( 1 ... M ) )
154 simpr3 
 |-  ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) )
155 10 adantlr 
 |-  ( ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) /\ f e. Y ) -> f : T --> RR )
156 132 148 2 3 5 149 150 151 152 153 154 155 fmuldfeqlem1 
 |-  ( ( ( ph /\ ( n e. ( 1 ... M ) /\ ( n + 1 ) e. ( 1 ... M ) /\ ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) ) /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) )
157 104 116 113 156 syl21anc 
 |-  ( ( n e. NN /\ ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) /\ ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) ) -> ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) )
158 157 3exp 
 |-  ( n e. NN -> ( ( ( ph /\ t e. T /\ n e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` n ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` n ) ) -> ( ( ph /\ t e. T /\ ( n + 1 ) e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` ( n + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( n + 1 ) ) ) ) )
159 29 36 43 50 103 158 nnind 
 |-  ( M e. NN -> ( ( ph /\ t e. T /\ M e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` M ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) ) )
160 22 159 mpcom 
 |-  ( ( ph /\ t e. T /\ M e. ( 1 ... M ) ) -> ( ( seq 1 ( P , U ) ` M ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
161 21 160 mpd3an3 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` M ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
162 4 fveq1i 
 |-  ( X ` t ) = ( ( seq 1 ( P , U ) ` M ) ` t )
163 162 a1i 
 |-  ( ( ph /\ t e. T ) -> ( X ` t ) = ( ( seq 1 ( P , U ) ` M ) ` t ) )
164 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
165 elnnuz 
 |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )
166 8 165 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
167 166 adantr 
 |-  ( ( ph /\ t e. T ) -> M e. ( ZZ>= ` 1 ) )
168 1 58 nfan 
 |-  F/ i ( ph /\ t e. T )
169 nfv 
 |-  F/ i k e. ( 1 ... M )
170 168 169 nfan 
 |-  F/ i ( ( ph /\ t e. T ) /\ k e. ( 1 ... M ) )
171 nfcv 
 |-  F/_ i k
172 64 171 nffv 
 |-  F/_ i ( ( F ` t ) ` k )
173 172 nfel1 
 |-  F/ i ( ( F ` t ) ` k ) e. RR
174 170 173 nfim 
 |-  F/ i ( ( ( ph /\ t e. T ) /\ k e. ( 1 ... M ) ) -> ( ( F ` t ) ` k ) e. RR )
175 eleq1 
 |-  ( i = k -> ( i e. ( 1 ... M ) <-> k e. ( 1 ... M ) ) )
176 175 anbi2d 
 |-  ( i = k -> ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) <-> ( ( ph /\ t e. T ) /\ k e. ( 1 ... M ) ) ) )
177 fveq2 
 |-  ( i = k -> ( ( F ` t ) ` i ) = ( ( F ` t ) ` k ) )
178 177 eleq1d 
 |-  ( i = k -> ( ( ( F ` t ) ` i ) e. RR <-> ( ( F ` t ) ` k ) e. RR ) )
179 176 178 imbi12d 
 |-  ( i = k -> ( ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) e. RR ) <-> ( ( ( ph /\ t e. T ) /\ k e. ( 1 ... M ) ) -> ( ( F ` t ) ` k ) e. RR ) ) )
180 78 ad2antlr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) )
181 simpr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> i e. ( 1 ... M ) )
182 9 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. Y )
183 simpl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ph )
184 183 182 jca 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ph /\ ( U ` i ) e. Y ) )
185 eleq1 
 |-  ( f = ( U ` i ) -> ( f e. Y <-> ( U ` i ) e. Y ) )
186 185 anbi2d 
 |-  ( f = ( U ` i ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( U ` i ) e. Y ) ) )
187 feq1 
 |-  ( f = ( U ` i ) -> ( f : T --> RR <-> ( U ` i ) : T --> RR ) )
188 186 187 imbi12d 
 |-  ( f = ( U ` i ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` i ) e. Y ) -> ( U ` i ) : T --> RR ) ) )
189 188 92 vtoclga 
 |-  ( ( U ` i ) e. Y -> ( ( ph /\ ( U ` i ) e. Y ) -> ( U ` i ) : T --> RR ) )
190 182 184 189 sylc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )
191 190 adantlr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )
192 simplr 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> t e. T )
193 191 192 ffvelrnd 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) ` t ) e. RR )
194 82 fvmpt2 
 |-  ( ( i e. ( 1 ... M ) /\ ( ( U ` i ) ` t ) e. RR ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) = ( ( U ` i ) ` t ) )
195 181 193 194 syl2anc 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) = ( ( U ` i ) ` t ) )
196 195 193 eqeltrd 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) e. RR )
197 180 196 eqeltrd 
 |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) e. RR )
198 174 179 197 chvarfv 
 |-  ( ( ( ph /\ t e. T ) /\ k e. ( 1 ... M ) ) -> ( ( F ` t ) ` k ) e. RR )
199 remulcl 
 |-  ( ( k e. RR /\ b e. RR ) -> ( k x. b ) e. RR )
200 199 adantl 
 |-  ( ( ( ph /\ t e. T ) /\ ( k e. RR /\ b e. RR ) ) -> ( k x. b ) e. RR )
201 167 198 200 seqcl 
 |-  ( ( ph /\ t e. T ) -> ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR )
202 6 fvmpt2 
 |-  ( ( t e. T /\ ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
203 164 201 202 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )
204 161 163 203 3eqtr4d 
 |-  ( ( ph /\ t e. T ) -> ( X ` t ) = ( Z ` t ) )