Metamath Proof Explorer

Theorem caofinvl

Description: Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses caofref.1 
|- ( ph -> A e. V )
caofref.2 
|- ( ph -> F : A --> S )
caofinv.3 
|- ( ph -> B e. W )
caofinv.4 
|- ( ph -> N : S --> S )
caofinv.5 
|- ( ph -> G = ( v e. A |-> ( N ` ( F ` v ) ) ) )
caofinvl.6 
|- ( ( ph /\ x e. S ) -> ( ( N ` x ) R x ) = B )
Assertion caofinvl 
|- ( ph -> ( G oF R F ) = ( A X. { B } ) )

Proof

Step Hyp Ref Expression
1 caofref.1 
 |-  ( ph -> A e. V )
2 caofref.2 
 |-  ( ph -> F : A --> S )
3 caofinv.3 
 |-  ( ph -> B e. W )
4 caofinv.4 
 |-  ( ph -> N : S --> S )
5 caofinv.5 
 |-  ( ph -> G = ( v e. A |-> ( N ` ( F ` v ) ) ) )
6 caofinvl.6 
 |-  ( ( ph /\ x e. S ) -> ( ( N ` x ) R x ) = B )
7 4 adantr 
 |-  ( ( ph /\ v e. A ) -> N : S --> S )
8 2 ffvelcdmda 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) e. S )
9 7 8 ffvelcdmd 
 |-  ( ( ph /\ v e. A ) -> ( N ` ( F ` v ) ) e. S )
10 5 9 fmpt3d 
 |-  ( ph -> G : A --> S )
11 10 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
12 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
13 fvex 
 |-  ( N ` ( F ` v ) ) e. _V
14 eqid 
 |-  ( v e. A |-> ( N ` ( F ` v ) ) ) = ( v e. A |-> ( N ` ( F ` v ) ) )
15 13 14 fnmpti 
 |-  ( v e. A |-> ( N ` ( F ` v ) ) ) Fn A
16 5 fneq1d 
 |-  ( ph -> ( G Fn A <-> ( v e. A |-> ( N ` ( F ` v ) ) ) Fn A ) )
17 15 16 mpbiri 
 |-  ( ph -> G Fn A )
18 dffn5 
 |-  ( G Fn A <-> G = ( w e. A |-> ( G ` w ) ) )
19 17 18 sylib 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
20 2 feqmptd 
 |-  ( ph -> F = ( w e. A |-> ( F ` w ) ) )
21 1 11 12 19 20 offval2 
 |-  ( ph -> ( G oF R F ) = ( w e. A |-> ( ( G ` w ) R ( F ` w ) ) ) )
22 5 fveq1d 
 |-  ( ph -> ( G ` w ) = ( ( v e. A |-> ( N ` ( F ` v ) ) ) ` w ) )
23 2fveq3 
 |-  ( v = w -> ( N ` ( F ` v ) ) = ( N ` ( F ` w ) ) )
24 fvex 
 |-  ( N ` ( F ` w ) ) e. _V
25 23 14 24 fvmpt 
 |-  ( w e. A -> ( ( v e. A |-> ( N ` ( F ` v ) ) ) ` w ) = ( N ` ( F ` w ) ) )
26 22 25 sylan9eq 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) = ( N ` ( F ` w ) ) )
27 26 oveq1d 
 |-  ( ( ph /\ w e. A ) -> ( ( G ` w ) R ( F ` w ) ) = ( ( N ` ( F ` w ) ) R ( F ` w ) ) )
28 fveq2 
 |-  ( x = ( F ` w ) -> ( N ` x ) = ( N ` ( F ` w ) ) )
29 id 
 |-  ( x = ( F ` w ) -> x = ( F ` w ) )
30 28 29 oveq12d 
 |-  ( x = ( F ` w ) -> ( ( N ` x ) R x ) = ( ( N ` ( F ` w ) ) R ( F ` w ) ) )
31 30 eqeq1d 
 |-  ( x = ( F ` w ) -> ( ( ( N ` x ) R x ) = B <-> ( ( N ` ( F ` w ) ) R ( F ` w ) ) = B ) )
32 6 ralrimiva 
 |-  ( ph -> A. x e. S ( ( N ` x ) R x ) = B )
33 32 adantr 
 |-  ( ( ph /\ w e. A ) -> A. x e. S ( ( N ` x ) R x ) = B )
34 31 33 12 rspcdva 
 |-  ( ( ph /\ w e. A ) -> ( ( N ` ( F ` w ) ) R ( F ` w ) ) = B )
35 27 34 eqtrd 
 |-  ( ( ph /\ w e. A ) -> ( ( G ` w ) R ( F ` w ) ) = B )
36 35 mpteq2dva 
 |-  ( ph -> ( w e. A |-> ( ( G ` w ) R ( F ` w ) ) ) = ( w e. A |-> B ) )
37 21 36 eqtrd 
 |-  ( ph -> ( G oF R F ) = ( w e. A |-> B ) )
38 fconstmpt 
 |-  ( A X. { B } ) = ( w e. A |-> B )
39 37 38 eqtr4di 
 |-  ( ph -> ( G oF R F ) = ( A X. { B } ) )