This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caofidlcan

Description: Transfer a cancellation/identity law to the function operation. (Contributed by SN, 16-Oct-2025)

Ref Expression
Hypotheses caofref.1 
|- ( ph -> A e. V )
caofref.2 
|- ( ph -> F : A --> S )
caofcom.3 
|- ( ph -> G : A --> S )
caofidlcan.4 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( ( x R y ) = y <-> x = .0. ) )
Assertion caofidlcan 
|- ( ph -> ( ( F oF R G ) = G <-> F = ( A X. { .0. } ) ) )

Proof

Step Hyp Ref Expression
1 caofref.1 
 |-  ( ph -> A e. V )
2 caofref.2 
 |-  ( ph -> F : A --> S )
3 caofcom.3 
 |-  ( ph -> G : A --> S )
4 caofidlcan.4 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( ( x R y ) = y <-> x = .0. ) )
5 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
6 3 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
7 5 6 jca 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) e. S /\ ( G ` w ) e. S ) )
8 4 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S ( ( x R y ) = y <-> x = .0. ) )
9 oveq1 
 |-  ( x = ( F ` w ) -> ( x R y ) = ( ( F ` w ) R y ) )
10 9 eqeq1d 
 |-  ( x = ( F ` w ) -> ( ( x R y ) = y <-> ( ( F ` w ) R y ) = y ) )
11 eqeq1 
 |-  ( x = ( F ` w ) -> ( x = .0. <-> ( F ` w ) = .0. ) )
12 10 11 bibi12d 
 |-  ( x = ( F ` w ) -> ( ( ( x R y ) = y <-> x = .0. ) <-> ( ( ( F ` w ) R y ) = y <-> ( F ` w ) = .0. ) ) )
13 oveq2 
 |-  ( y = ( G ` w ) -> ( ( F ` w ) R y ) = ( ( F ` w ) R ( G ` w ) ) )
14 id 
 |-  ( y = ( G ` w ) -> y = ( G ` w ) )
15 13 14 eqeq12d 
 |-  ( y = ( G ` w ) -> ( ( ( F ` w ) R y ) = y <-> ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) ) )
16 15 bibi1d 
 |-  ( y = ( G ` w ) -> ( ( ( ( F ` w ) R y ) = y <-> ( F ` w ) = .0. ) <-> ( ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) <-> ( F ` w ) = .0. ) ) )
17 12 16 rspc2v 
 |-  ( ( ( F ` w ) e. S /\ ( G ` w ) e. S ) -> ( A. x e. S A. y e. S ( ( x R y ) = y <-> x = .0. ) -> ( ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) <-> ( F ` w ) = .0. ) ) )
18 8 17 mpan9 
 |-  ( ( ph /\ ( ( F ` w ) e. S /\ ( G ` w ) e. S ) ) -> ( ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) <-> ( F ` w ) = .0. ) )
19 7 18 syldan 
 |-  ( ( ph /\ w e. A ) -> ( ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) <-> ( F ` w ) = .0. ) )
20 19 ralbidva 
 |-  ( ph -> ( A. w e. A ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) <-> A. w e. A ( F ` w ) = .0. ) )
21 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) R ( G ` w ) ) e. _V )
22 21 ralrimiva 
 |-  ( ph -> A. w e. A ( ( F ` w ) R ( G ` w ) ) e. _V )
23 mpteqb 
 |-  ( A. w e. A ( ( F ` w ) R ( G ` w ) ) e. _V -> ( ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) = ( w e. A |-> ( G ` w ) ) <-> A. w e. A ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) ) )
24 22 23 syl 
 |-  ( ph -> ( ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) = ( w e. A |-> ( G ` w ) ) <-> A. w e. A ( ( F ` w ) R ( G ` w ) ) = ( G ` w ) ) )
25 5 ralrimiva 
 |-  ( ph -> A. w e. A ( F ` w ) e. S )
26 mpteqb 
 |-  ( A. w e. A ( F ` w ) e. S -> ( ( w e. A |-> ( F ` w ) ) = ( w e. A |-> .0. ) <-> A. w e. A ( F ` w ) = .0. ) )
27 25 26 syl 
 |-  ( ph -> ( ( w e. A |-> ( F ` w ) ) = ( w e. A |-> .0. ) <-> A. w e. A ( F ` w ) = .0. ) )
28 20 24 27 3bitr4d 
 |-  ( ph -> ( ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) = ( w e. A |-> ( G ` w ) ) <-> ( w e. A |-> ( F ` w ) ) = ( w e. A |-> .0. ) ) )
29 2 feqmptd 
 |-  ( ph -> F = ( w e. A |-> ( F ` w ) ) )
30 3 feqmptd 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
31 1 5 6 29 30 offval2 
 |-  ( ph -> ( F oF R G ) = ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) )
32 31 30 eqeq12d 
 |-  ( ph -> ( ( F oF R G ) = G <-> ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) = ( w e. A |-> ( G ` w ) ) ) )
33 fconstmpt 
 |-  ( A X. { .0. } ) = ( w e. A |-> .0. )
34 33 a1i 
 |-  ( ph -> ( A X. { .0. } ) = ( w e. A |-> .0. ) )
35 29 34 eqeq12d 
 |-  ( ph -> ( F = ( A X. { .0. } ) <-> ( w e. A |-> ( F ` w ) ) = ( w e. A |-> .0. ) ) )
36 28 32 35 3bitr4d 
 |-  ( ph -> ( ( F oF R G ) = G <-> F = ( A X. { .0. } ) ) )