Metamath Proof Explorer

Theorem fcores

Description: Every composite function ( G o. F ) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024)

Ref Expression
Hypotheses fcores.f 
|- ( ph -> F : A --> B )
fcores.e 
|- E = ( ran F i^i C )
fcores.p 
|- P = ( `' F " C )
fcores.x 
|- X = ( F |` P )
fcores.g 
|- ( ph -> G : C --> D )
fcores.y 
|- Y = ( G |` E )
Assertion fcores 
|- ( ph -> ( G o. F ) = ( Y o. X ) )

Proof

Step Hyp Ref Expression
1 fcores.f 
 |-  ( ph -> F : A --> B )
2 fcores.e 
 |-  E = ( ran F i^i C )
3 fcores.p 
 |-  P = ( `' F " C )
4 fcores.x 
 |-  X = ( F |` P )
5 fcores.g 
 |-  ( ph -> G : C --> D )
6 fcores.y 
 |-  Y = ( G |` E )
7 1 ffund 
 |-  ( ph -> Fun F )
8 fcof 
 |-  ( ( G : C --> D /\ Fun F ) -> ( G o. F ) : ( `' F " C ) --> D )
9 5 7 8 syl2anc 
 |-  ( ph -> ( G o. F ) : ( `' F " C ) --> D )
10 9 ffnd 
 |-  ( ph -> ( G o. F ) Fn ( `' F " C ) )
11 3 fneq2i 
 |-  ( ( G o. F ) Fn P <-> ( G o. F ) Fn ( `' F " C ) )
12 10 11 sylibr 
 |-  ( ph -> ( G o. F ) Fn P )
13 1 2 3 4 5 6 fcoreslem4 
 |-  ( ph -> ( Y o. X ) Fn P )
14 4 fveq1i 
 |-  ( X ` x ) = ( ( F |` P ) ` x )
15 simpr 
 |-  ( ( ph /\ x e. P ) -> x e. P )
16 15 fvresd 
 |-  ( ( ph /\ x e. P ) -> ( ( F |` P ) ` x ) = ( F ` x ) )
17 14 16 syl5eq 
 |-  ( ( ph /\ x e. P ) -> ( X ` x ) = ( F ` x ) )
18 17 fveq2d 
 |-  ( ( ph /\ x e. P ) -> ( Y ` ( X ` x ) ) = ( Y ` ( F ` x ) ) )
19 6 fveq1i 
 |-  ( Y ` ( F ` x ) ) = ( ( G |` E ) ` ( F ` x ) )
20 cnvimass 
 |-  ( `' F " C ) C_ dom F
21 3 20 eqsstri 
 |-  P C_ dom F
22 21 sseli 
 |-  ( x e. P -> x e. dom F )
23 fvelrn 
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
24 7 22 23 syl2an 
 |-  ( ( ph /\ x e. P ) -> ( F ` x ) e. ran F )
25 3 eleq2i 
 |-  ( x e. P <-> x e. ( `' F " C ) )
26 25 biimpi 
 |-  ( x e. P -> x e. ( `' F " C ) )
27 fvimacnvi 
 |-  ( ( Fun F /\ x e. ( `' F " C ) ) -> ( F ` x ) e. C )
28 7 26 27 syl2an 
 |-  ( ( ph /\ x e. P ) -> ( F ` x ) e. C )
29 24 28 elind 
 |-  ( ( ph /\ x e. P ) -> ( F ` x ) e. ( ran F i^i C ) )
30 29 2 eleqtrrdi 
 |-  ( ( ph /\ x e. P ) -> ( F ` x ) e. E )
31 30 fvresd 
 |-  ( ( ph /\ x e. P ) -> ( ( G |` E ) ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
32 19 31 syl5eq 
 |-  ( ( ph /\ x e. P ) -> ( Y ` ( F ` x ) ) = ( G ` ( F ` x ) ) )
33 18 32 eqtrd 
 |-  ( ( ph /\ x e. P ) -> ( Y ` ( X ` x ) ) = ( G ` ( F ` x ) ) )
34 1 2 3 4 fcoreslem3 
 |-  ( ph -> X : P -onto-> E )
35 fof 
 |-  ( X : P -onto-> E -> X : P --> E )
36 34 35 syl 
 |-  ( ph -> X : P --> E )
37 36 adantr 
 |-  ( ( ph /\ x e. P ) -> X : P --> E )
38 37 15 fvco3d 
 |-  ( ( ph /\ x e. P ) -> ( ( Y o. X ) ` x ) = ( Y ` ( X ` x ) ) )
39 1 adantr 
 |-  ( ( ph /\ x e. P ) -> F : A --> B )
40 21 a1i 
 |-  ( ph -> P C_ dom F )
41 40 sselda 
 |-  ( ( ph /\ x e. P ) -> x e. dom F )
42 1 fdmd 
 |-  ( ph -> dom F = A )
43 42 eqcomd 
 |-  ( ph -> A = dom F )
44 43 eleq2d 
 |-  ( ph -> ( x e. A <-> x e. dom F ) )
45 44 adantr 
 |-  ( ( ph /\ x e. P ) -> ( x e. A <-> x e. dom F ) )
46 41 45 mpbird 
 |-  ( ( ph /\ x e. P ) -> x e. A )
47 39 46 fvco3d 
 |-  ( ( ph /\ x e. P ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
48 33 38 47 3eqtr4rd 
 |-  ( ( ph /\ x e. P ) -> ( ( G o. F ) ` x ) = ( ( Y o. X ) ` x ) )
49 12 13 48 eqfnfvd 
 |-  ( ph -> ( G o. F ) = ( Y o. X ) )