Metamath Proof Explorer

Theorem mbfmullem

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 )
Assertion mbfmullem 
|- ( 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 1 3 mbfi1flim 
 |-  ( ph -> E. f ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) )
6 2 4 mbfi1flim 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) )
7 exdistrv 
 |-  ( E. f E. g ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) <-> ( E. f ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ E. g ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) )
8 1 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> F e. MblFn )
9 2 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> G e. MblFn )
10 3 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> F : A --> RR )
11 4 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> G : A --> RR )
12 simprll 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> f : NN --> dom S.1 )
13 simprlr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) )
14 fveq2 
 |-  ( y = x -> ( ( f ` n ) ` y ) = ( ( f ` n ) ` x ) )
15 14 mpteq2dv 
 |-  ( y = x -> ( n e. NN |-> ( ( f ` n ) ` y ) ) = ( n e. NN |-> ( ( f ` n ) ` x ) ) )
16 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
17 16 fveq1d 
 |-  ( n = m -> ( ( f ` n ) ` x ) = ( ( f ` m ) ` x ) )
18 17 cbvmptv 
 |-  ( n e. NN |-> ( ( f ` n ) ` x ) ) = ( m e. NN |-> ( ( f ` m ) ` x ) )
19 15 18 eqtrdi 
 |-  ( y = x -> ( n e. NN |-> ( ( f ` n ) ` y ) ) = ( m e. NN |-> ( ( f ` m ) ` x ) ) )
20 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
21 19 20 breq12d 
 |-  ( y = x -> ( ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) <-> ( m e. NN |-> ( ( f ` m ) ` x ) ) ~~> ( F ` x ) ) )
22 21 rspccva 
 |-  ( ( A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) /\ x e. A ) -> ( m e. NN |-> ( ( f ` m ) ` x ) ) ~~> ( F ` x ) )
23 13 22 sylan 
 |-  ( ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) /\ x e. A ) -> ( m e. NN |-> ( ( f ` m ) ` x ) ) ~~> ( F ` x ) )
24 simprrl 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> g : NN --> dom S.1 )
25 simprrr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) )
26 fveq2 
 |-  ( y = x -> ( ( g ` n ) ` y ) = ( ( g ` n ) ` x ) )
27 26 mpteq2dv 
 |-  ( y = x -> ( n e. NN |-> ( ( g ` n ) ` y ) ) = ( n e. NN |-> ( ( g ` n ) ` x ) ) )
28 fveq2 
 |-  ( n = m -> ( g ` n ) = ( g ` m ) )
29 28 fveq1d 
 |-  ( n = m -> ( ( g ` n ) ` x ) = ( ( g ` m ) ` x ) )
30 29 cbvmptv 
 |-  ( n e. NN |-> ( ( g ` n ) ` x ) ) = ( m e. NN |-> ( ( g ` m ) ` x ) )
31 27 30 eqtrdi 
 |-  ( y = x -> ( n e. NN |-> ( ( g ` n ) ` y ) ) = ( m e. NN |-> ( ( g ` m ) ` x ) ) )
32 fveq2 
 |-  ( y = x -> ( G ` y ) = ( G ` x ) )
33 31 32 breq12d 
 |-  ( y = x -> ( ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) <-> ( m e. NN |-> ( ( g ` m ) ` x ) ) ~~> ( G ` x ) ) )
34 33 rspccva 
 |-  ( ( A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) /\ x e. A ) -> ( m e. NN |-> ( ( g ` m ) ` x ) ) ~~> ( G ` x ) )
35 25 34 sylan 
 |-  ( ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) /\ x e. A ) -> ( m e. NN |-> ( ( g ` m ) ` x ) ) ~~> ( G ` x ) )
36 8 9 10 11 12 23 24 35 mbfmullem2 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) ) -> ( F oF x. G ) e. MblFn )
37 36 ex 
 |-  ( ph -> ( ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) -> ( F oF x. G ) e. MblFn ) )
38 37 exlimdvv 
 |-  ( ph -> ( E. f E. g ( ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) -> ( F oF x. G ) e. MblFn ) )
39 7 38 syl5bir 
 |-  ( ph -> ( ( E. f ( f : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( f ` n ) ` y ) ) ~~> ( F ` y ) ) /\ E. g ( g : NN --> dom S.1 /\ A. y e. A ( n e. NN |-> ( ( g ` n ) ` y ) ) ~~> ( G ` y ) ) ) -> ( F oF x. G ) e. MblFn ) )
40 5 6 39 mp2and 
 |-  ( ph -> ( F oF x. G ) e. MblFn )