Metamath Proof Explorer


Theorem fmuldfeqlem1

Description: induction step for the proof of fmuldfeq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 fmuldfeqlem1.1
 |-  F/ f ph
2 fmuldfeqlem1.2
 |-  F/ g ph
3 fmuldfeqlem1.3
 |-  F/_ t Y
4 fmuldfeqlem1.5
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
5 fmuldfeqlem1.6
 |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
6 fmuldfeqlem1.7
 |-  ( ph -> T e. _V )
7 fmuldfeqlem1.8
 |-  ( ph -> U : ( 1 ... M ) --> Y )
8 fmuldfeqlem1.9
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
9 fmuldfeqlem1.10
 |-  ( ph -> N e. ( 1 ... M ) )
10 fmuldfeqlem1.11
 |-  ( ph -> ( N + 1 ) e. ( 1 ... M ) )
11 fmuldfeqlem1.12
 |-  ( ph -> ( ( seq 1 ( P , U ) ` N ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` N ) )
12 fmuldfeqlem1.13
 |-  ( ( ph /\ f e. Y ) -> f : T --> RR )
13 ovex
 |-  ( 1 ... M ) e. _V
14 13 mptex
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V
15 5 fvmpt2
 |-  ( ( t e. T /\ ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
16 14 15 mpan2
 |-  ( t e. T -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
17 fveq2
 |-  ( i = j -> ( U ` i ) = ( U ` j ) )
18 17 fveq1d
 |-  ( i = j -> ( ( U ` i ) ` t ) = ( ( U ` j ) ` t ) )
19 18 cbvmptv
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) )
20 16 19 eqtrdi
 |-  ( t e. T -> ( F ` t ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) ) )
21 20 adantl
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) ) )
22 fveq2
 |-  ( j = ( N + 1 ) -> ( U ` j ) = ( U ` ( N + 1 ) ) )
23 22 fveq1d
 |-  ( j = ( N + 1 ) -> ( ( U ` j ) ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
24 23 adantl
 |-  ( ( ( ph /\ t e. T ) /\ j = ( N + 1 ) ) -> ( ( U ` j ) ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
25 10 adantr
 |-  ( ( ph /\ t e. T ) -> ( N + 1 ) e. ( 1 ... M ) )
26 7 10 ffvelrnd
 |-  ( ph -> ( U ` ( N + 1 ) ) e. Y )
27 26 ancli
 |-  ( ph -> ( ph /\ ( U ` ( N + 1 ) ) e. Y ) )
28 nfcv
 |-  F/_ f ( U ` ( N + 1 ) )
29 nfv
 |-  F/ f ( U ` ( N + 1 ) ) e. Y
30 1 29 nfan
 |-  F/ f ( ph /\ ( U ` ( N + 1 ) ) e. Y )
31 nfv
 |-  F/ f ( U ` ( N + 1 ) ) : T --> RR
32 30 31 nfim
 |-  F/ f ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR )
33 eleq1
 |-  ( f = ( U ` ( N + 1 ) ) -> ( f e. Y <-> ( U ` ( N + 1 ) ) e. Y ) )
34 33 anbi2d
 |-  ( f = ( U ` ( N + 1 ) ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( U ` ( N + 1 ) ) e. Y ) ) )
35 feq1
 |-  ( f = ( U ` ( N + 1 ) ) -> ( f : T --> RR <-> ( U ` ( N + 1 ) ) : T --> RR ) )
36 34 35 imbi12d
 |-  ( f = ( U ` ( N + 1 ) ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR ) ) )
37 28 32 36 12 vtoclgf
 |-  ( ( U ` ( N + 1 ) ) e. Y -> ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR ) )
38 26 27 37 sylc
 |-  ( ph -> ( U ` ( N + 1 ) ) : T --> RR )
39 38 ffvelrnda
 |-  ( ( ph /\ t e. T ) -> ( ( U ` ( N + 1 ) ) ` t ) e. RR )
40 21 24 25 39 fvmptd
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` ( N + 1 ) ) = ( ( U ` ( N + 1 ) ) ` t ) )
41 40 oveq2d
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
42 elfzuz
 |-  ( N e. ( 1 ... M ) -> N e. ( ZZ>= ` 1 ) )
43 9 42 syl
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
44 seqp1
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
45 43 44 syl
 |-  ( ph -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
46 45 adantr
 |-  ( ( ph /\ t e. T ) -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
47 seqp1
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) )
48 43 47 syl
 |-  ( ph -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) )
49 nfcv
 |-  F/_ h ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
50 nfcv
 |-  F/_ l ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
51 nfcv
 |-  F/_ f ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) )
52 nfcv
 |-  F/_ g ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) )
53 fveq1
 |-  ( f = h -> ( f ` t ) = ( h ` t ) )
54 fveq1
 |-  ( g = l -> ( g ` t ) = ( l ` t ) )
55 53 54 oveqan12d
 |-  ( ( f = h /\ g = l ) -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
56 55 mpteq2dv
 |-  ( ( f = h /\ g = l ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
57 49 50 51 52 56 cbvmpo
 |-  ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) ) = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
58 4 57 eqtri
 |-  P = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
59 58 a1i
 |-  ( ph -> P = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) ) )
60 nfcv
 |-  F/_ t 1
61 nfmpt1
 |-  F/_ t ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
62 3 3 61 nfmpo
 |-  F/_ t ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
63 4 62 nfcxfr
 |-  F/_ t P
64 nfcv
 |-  F/_ t U
65 60 63 64 nfseq
 |-  F/_ t seq 1 ( P , U )
66 nfcv
 |-  F/_ t N
67 65 66 nffv
 |-  F/_ t ( seq 1 ( P , U ) ` N )
68 67 nfeq2
 |-  F/ t h = ( seq 1 ( P , U ) ` N )
69 nfv
 |-  F/ t l = ( U ` ( N + 1 ) )
70 68 69 nfan
 |-  F/ t ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) )
71 fveq1
 |-  ( h = ( seq 1 ( P , U ) ` N ) -> ( h ` t ) = ( ( seq 1 ( P , U ) ` N ) ` t ) )
72 71 ad2antrr
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( h ` t ) = ( ( seq 1 ( P , U ) ` N ) ` t ) )
73 fveq1
 |-  ( l = ( U ` ( N + 1 ) ) -> ( l ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
74 73 ad2antlr
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( l ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
75 72 74 oveq12d
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( ( h ` t ) x. ( l ` t ) ) = ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
76 70 75 mpteq2da
 |-  ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
77 76 adantl
 |-  ( ( ph /\ ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
78 eqid
 |-  ( seq 1 ( P , U ) ` N ) = ( seq 1 ( P , U ) ` N )
79 3simpc
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( h e. Y /\ l e. Y ) )
80 nfcv
 |-  F/_ f h
81 nfcv
 |-  F/_ g h
82 nfcv
 |-  F/_ g l
83 nfv
 |-  F/ f h e. Y
84 nfv
 |-  F/ f g e. Y
85 1 83 84 nf3an
 |-  F/ f ( ph /\ h e. Y /\ g e. Y )
86 nfv
 |-  F/ f ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y
87 85 86 nfim
 |-  F/ f ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y )
88 nfv
 |-  F/ g h e. Y
89 nfv
 |-  F/ g l e. Y
90 2 88 89 nf3an
 |-  F/ g ( ph /\ h e. Y /\ l e. Y )
91 nfv
 |-  F/ g ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y
92 90 91 nfim
 |-  F/ g ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
93 eleq1
 |-  ( f = h -> ( f e. Y <-> h e. Y ) )
94 93 3anbi2d
 |-  ( f = h -> ( ( ph /\ f e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ g e. Y ) ) )
95 53 oveq1d
 |-  ( f = h -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( g ` t ) ) )
96 95 mpteq2dv
 |-  ( f = h -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) )
97 96 eleq1d
 |-  ( f = h -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) )
98 94 97 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 ) ) )
99 eleq1
 |-  ( g = l -> ( g e. Y <-> l e. Y ) )
100 99 3anbi3d
 |-  ( g = l -> ( ( ph /\ h e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ l e. Y ) ) )
101 54 oveq2d
 |-  ( g = l -> ( ( h ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
102 101 mpteq2dv
 |-  ( g = l -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
103 102 eleq1d
 |-  ( g = l -> ( ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
104 100 103 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 ) ) )
105 80 81 82 87 92 98 104 8 vtocl2gf
 |-  ( ( h e. Y /\ l e. Y ) -> ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
106 79 105 mpcom
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
107 58 78 9 7 106 6 fmulcl
 |-  ( ph -> ( seq 1 ( P , U ) ` N ) e. Y )
108 mptexg
 |-  ( T e. _V -> ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) e. _V )
109 6 108 syl
 |-  ( ph -> ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) e. _V )
110 59 77 107 26 109 ovmpod
 |-  ( ph -> ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
111 48 110 eqtrd
 |-  ( ph -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
112 107 ancli
 |-  ( ph -> ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) )
113 nfcv
 |-  F/_ f 1
114 nfmpo1
 |-  F/_ f ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
115 4 114 nfcxfr
 |-  F/_ f P
116 nfcv
 |-  F/_ f U
117 113 115 116 nfseq
 |-  F/_ f seq 1 ( P , U )
118 nfcv
 |-  F/_ f N
119 117 118 nffv
 |-  F/_ f ( seq 1 ( P , U ) ` N )
120 119 nfel1
 |-  F/ f ( seq 1 ( P , U ) ` N ) e. Y
121 1 120 nfan
 |-  F/ f ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y )
122 nfcv
 |-  F/_ f T
123 nfcv
 |-  F/_ f RR
124 119 122 123 nff
 |-  F/ f ( seq 1 ( P , U ) ` N ) : T --> RR
125 121 124 nfim
 |-  F/ f ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR )
126 eleq1
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( f e. Y <-> ( seq 1 ( P , U ) ` N ) e. Y ) )
127 126 anbi2d
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) ) )
128 feq1
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( f : T --> RR <-> ( seq 1 ( P , U ) ` N ) : T --> RR ) )
129 127 128 imbi12d
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR ) ) )
130 119 125 129 12 vtoclgf
 |-  ( ( seq 1 ( P , U ) ` N ) e. Y -> ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR ) )
131 107 112 130 sylc
 |-  ( ph -> ( seq 1 ( P , U ) ` N ) : T --> RR )
132 131 ffvelrnda
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` N ) ` t ) e. RR )
133 132 39 remulcld
 |-  ( ( ph /\ t e. T ) -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) e. RR )
134 111 133 fvmpt2d
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
135 11 oveq1d
 |-  ( ph -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
136 135 adantr
 |-  ( ( ph /\ t e. T ) -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
137 134 136 eqtrd
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
138 41 46 137 3eqtr4rd
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) )