Metamath Proof Explorer

Theorem mbfmullem2

Description: Lemma for mbfmul . (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfmul.1 
|- ( ph -> F e. MblFn )
mbfmul.2 
|- ( ph -> G e. MblFn )
mbfmul.3 
|- ( ph -> F : A --> RR )
mbfmul.4 
|- ( ph -> G : A --> RR )
mbfmul.5 
|- ( ph -> P : NN --> dom S.1 )
mbfmul.6 
|- ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
mbfmul.7 
|- ( ph -> Q : NN --> dom S.1 )
mbfmul.8 
|- ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( Q ` n ) ` x ) ) ~~> ( G ` x ) )
Assertion mbfmullem2 
|- ( ph -> ( F oF x. G ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfmul.1 
 |-  ( ph -> F e. MblFn )
2 mbfmul.2 
 |-  ( ph -> G e. MblFn )
3 mbfmul.3 
 |-  ( ph -> F : A --> RR )
4 mbfmul.4 
 |-  ( ph -> G : A --> RR )
5 mbfmul.5 
 |-  ( ph -> P : NN --> dom S.1 )
6 mbfmul.6 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
7 mbfmul.7 
 |-  ( ph -> Q : NN --> dom S.1 )
8 mbfmul.8 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( Q ` n ) ` x ) ) ~~> ( G ` x ) )
9 3 ffnd 
 |-  ( ph -> F Fn A )
10 4 ffnd 
 |-  ( ph -> G Fn A )
11 3 fdmd 
 |-  ( ph -> dom F = A )
12 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
13 1 12 syl 
 |-  ( ph -> dom F e. dom vol )
14 11 13 eqeltrrd 
 |-  ( ph -> A e. dom vol )
15 inidm 
 |-  ( A i^i A ) = A
16 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
17 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
18 9 10 14 14 15 16 17 offval 
 |-  ( ph -> ( F oF x. G ) = ( x e. A |-> ( ( F ` x ) x. ( G ` x ) ) ) )
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 1zzd 
 |-  ( ph -> 1 e. ZZ )
21 1zzd 
 |-  ( ( ph /\ x e. A ) -> 1 e. ZZ )
22 nnex 
 |-  NN e. _V
23 22 mptex 
 |-  ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) e. _V
24 23 a1i 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) e. _V )
25 5 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( P ` n ) e. dom S.1 )
26 i1ff 
 |-  ( ( P ` n ) e. dom S.1 -> ( P ` n ) : RR --> RR )
27 25 26 syl 
 |-  ( ( ph /\ n e. NN ) -> ( P ` n ) : RR --> RR )
28 27 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( P ` n ) : RR --> RR )
29 mblss 
 |-  ( A e. dom vol -> A C_ RR )
30 14 29 syl 
 |-  ( ph -> A C_ RR )
31 30 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
32 31 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> x e. RR )
33 28 32 ffvelcdmd 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( ( P ` n ) ` x ) e. RR )
34 33 recnd 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( ( P ` n ) ` x ) e. CC )
35 34 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( P ` n ) ` x ) ) : NN --> CC )
36 35 ffvelcdmda 
 |-  ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ` k ) e. CC )
37 7 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( Q ` n ) e. dom S.1 )
38 i1ff 
 |-  ( ( Q ` n ) e. dom S.1 -> ( Q ` n ) : RR --> RR )
39 37 38 syl 
 |-  ( ( ph /\ n e. NN ) -> ( Q ` n ) : RR --> RR )
40 39 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( Q ` n ) : RR --> RR )
41 40 32 ffvelcdmd 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( ( Q ` n ) ` x ) e. RR )
42 41 recnd 
 |-  ( ( ( ph /\ x e. A ) /\ n e. NN ) -> ( ( Q ` n ) ` x ) e. CC )
43 42 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( Q ` n ) ` x ) ) : NN --> CC )
44 43 ffvelcdmda 
 |-  ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( Q ` n ) ` x ) ) ` k ) e. CC )
45 fveq2 
 |-  ( n = k -> ( P ` n ) = ( P ` k ) )
46 45 fveq1d 
 |-  ( n = k -> ( ( P ` n ) ` x ) = ( ( P ` k ) ` x ) )
47 fveq2 
 |-  ( n = k -> ( Q ` n ) = ( Q ` k ) )
48 47 fveq1d 
 |-  ( n = k -> ( ( Q ` n ) ` x ) = ( ( Q ` k ) ` x ) )
49 46 48 oveq12d 
 |-  ( n = k -> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) = ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) )
50 eqid 
 |-  ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) = ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) )
51 ovex 
 |-  ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) e. _V
52 49 50 51 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) ` k ) = ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) )
53 52 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) ` k ) = ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) )
54 eqid 
 |-  ( n e. NN |-> ( ( P ` n ) ` x ) ) = ( n e. NN |-> ( ( P ` n ) ` x ) )
55 fvex 
 |-  ( ( P ` k ) ` x ) e. _V
56 46 54 55 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ` k ) = ( ( P ` k ) ` x ) )
57 eqid 
 |-  ( n e. NN |-> ( ( Q ` n ) ` x ) ) = ( n e. NN |-> ( ( Q ` n ) ` x ) )
58 fvex 
 |-  ( ( Q ` k ) ` x ) e. _V
59 48 57 58 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( Q ` n ) ` x ) ) ` k ) = ( ( Q ` k ) ` x ) )
60 56 59 oveq12d 
 |-  ( k e. NN -> ( ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ` k ) x. ( ( n e. NN |-> ( ( Q ` n ) ` x ) ) ` k ) ) = ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) )
61 60 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ` k ) x. ( ( n e. NN |-> ( ( Q ` n ) ` x ) ) ` k ) ) = ( ( ( P ` k ) ` x ) x. ( ( Q ` k ) ` x ) ) )
62 53 61 eqtr4d 
 |-  ( ( ( ph /\ x e. A ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) ` k ) = ( ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ` k ) x. ( ( n e. NN |-> ( ( Q ` n ) ` x ) ) ` k ) ) )
63 19 21 6 24 8 36 44 62 climmul 
 |-  ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) ~~> ( ( F ` x ) x. ( G ` x ) ) )
64 30 adantr 
 |-  ( ( ph /\ n e. NN ) -> A C_ RR )
65 64 resmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) |` A ) = ( x e. A |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) )
66 27 ffnd 
 |-  ( ( ph /\ n e. NN ) -> ( P ` n ) Fn RR )
67 39 ffnd 
 |-  ( ( ph /\ n e. NN ) -> ( Q ` n ) Fn RR )
68 reex 
 |-  RR e. _V
69 68 a1i 
 |-  ( ( ph /\ n e. NN ) -> RR e. _V )
70 inidm 
 |-  ( RR i^i RR ) = RR
71 eqidd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( P ` n ) ` x ) = ( ( P ` n ) ` x ) )
72 eqidd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( Q ` n ) ` x ) = ( ( Q ` n ) ` x ) )
73 66 67 69 69 70 71 72 offval 
 |-  ( ( ph /\ n e. NN ) -> ( ( P ` n ) oF x. ( Q ` n ) ) = ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) )
74 25 37 i1fmul 
 |-  ( ( ph /\ n e. NN ) -> ( ( P ` n ) oF x. ( Q ` n ) ) e. dom S.1 )
75 i1fmbf 
 |-  ( ( ( P ` n ) oF x. ( Q ` n ) ) e. dom S.1 -> ( ( P ` n ) oF x. ( Q ` n ) ) e. MblFn )
76 74 75 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( P ` n ) oF x. ( Q ` n ) ) e. MblFn )
77 73 76 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) e. MblFn )
78 14 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. dom vol )
79 mbfres 
 |-  ( ( ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) e. MblFn /\ A e. dom vol ) -> ( ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) |` A ) e. MblFn )
80 77 78 79 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( x e. RR |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) |` A ) e. MblFn )
81 65 80 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. A |-> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) ) e. MblFn )
82 ovex 
 |-  ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) e. _V
83 82 a1i 
 |-  ( ( ph /\ ( n e. NN /\ x e. A ) ) -> ( ( ( P ` n ) ` x ) x. ( ( Q ` n ) ` x ) ) e. _V )
84 19 20 63 81 83 mbflim 
 |-  ( ph -> ( x e. A |-> ( ( F ` x ) x. ( G ` x ) ) ) e. MblFn )
85 18 84 eqeltrd 
 |-  ( ph -> ( F oF x. G ) e. MblFn )