# Metamath Proof Explorer

## Theorem fvcofneq

Description: The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019)

Ref Expression
Assertion fvcofneq ${⊢}\left({G}Fn{A}\wedge {K}Fn{B}\right)\to \left(\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({G}Fn{A}\wedge {K}Fn{B}\right)\to {G}Fn{A}$
2 elinel1 ${⊢}{X}\in \left({A}\cap {B}\right)\to {X}\in {A}$
3 2 3ad2ant1 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to {X}\in {A}$
4 fvco2 ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left({F}\circ {G}\right)\left({X}\right)={F}\left({G}\left({X}\right)\right)$
5 1 3 4 syl2an ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)={F}\left({G}\left({X}\right)\right)$
6 simpr ${⊢}\left({G}Fn{A}\wedge {K}Fn{B}\right)\to {K}Fn{B}$
7 elinel2 ${⊢}{X}\in \left({A}\cap {B}\right)\to {X}\in {B}$
8 7 3ad2ant1 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to {X}\in {B}$
9 fvco2 ${⊢}\left({K}Fn{B}\wedge {X}\in {B}\right)\to \left({H}\circ {K}\right)\left({X}\right)={H}\left({K}\left({X}\right)\right)$
10 6 8 9 syl2an ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to \left({H}\circ {K}\right)\left({X}\right)={H}\left({K}\left({X}\right)\right)$
11 fveq2 ${⊢}{K}\left({X}\right)={G}\left({X}\right)\to {H}\left({K}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)$
12 11 eqcoms ${⊢}{G}\left({X}\right)={K}\left({X}\right)\to {H}\left({K}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)$
13 12 3ad2ant2 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to {H}\left({K}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)$
14 13 adantl ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to {H}\left({K}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)$
15 id ${⊢}{G}Fn{A}\to {G}Fn{A}$
16 fnfvelrn ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to {G}\left({X}\right)\in \mathrm{ran}{G}$
17 15 2 16 syl2anr ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}Fn{A}\right)\to {G}\left({X}\right)\in \mathrm{ran}{G}$
18 17 ex ${⊢}{X}\in \left({A}\cap {B}\right)\to \left({G}Fn{A}\to {G}\left({X}\right)\in \mathrm{ran}{G}\right)$
19 id ${⊢}{K}Fn{B}\to {K}Fn{B}$
20 fnfvelrn ${⊢}\left({K}Fn{B}\wedge {X}\in {B}\right)\to {K}\left({X}\right)\in \mathrm{ran}{K}$
21 19 7 20 syl2anr ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {K}Fn{B}\right)\to {K}\left({X}\right)\in \mathrm{ran}{K}$
22 21 ex ${⊢}{X}\in \left({A}\cap {B}\right)\to \left({K}Fn{B}\to {K}\left({X}\right)\in \mathrm{ran}{K}\right)$
23 18 22 anim12d ${⊢}{X}\in \left({A}\cap {B}\right)\to \left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\to \left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {K}\left({X}\right)\in \mathrm{ran}{K}\right)\right)$
24 eleq1 ${⊢}{K}\left({X}\right)={G}\left({X}\right)\to \left({K}\left({X}\right)\in \mathrm{ran}{K}↔{G}\left({X}\right)\in \mathrm{ran}{K}\right)$
25 24 eqcoms ${⊢}{G}\left({X}\right)={K}\left({X}\right)\to \left({K}\left({X}\right)\in \mathrm{ran}{K}↔{G}\left({X}\right)\in \mathrm{ran}{K}\right)$
26 25 anbi2d ${⊢}{G}\left({X}\right)={K}\left({X}\right)\to \left(\left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {K}\left({X}\right)\in \mathrm{ran}{K}\right)↔\left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {G}\left({X}\right)\in \mathrm{ran}{K}\right)\right)$
27 elin ${⊢}{G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)↔\left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {G}\left({X}\right)\in \mathrm{ran}{K}\right)$
28 27 biimpri ${⊢}\left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {G}\left({X}\right)\in \mathrm{ran}{K}\right)\to {G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)$
29 26 28 syl6bi ${⊢}{G}\left({X}\right)={K}\left({X}\right)\to \left(\left({G}\left({X}\right)\in \mathrm{ran}{G}\wedge {K}\left({X}\right)\in \mathrm{ran}{K}\right)\to {G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\right)$
30 23 29 sylan9 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\right)\to \left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\to {G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\right)$
31 fveq2 ${⊢}{x}={G}\left({X}\right)\to {F}\left({x}\right)={F}\left({G}\left({X}\right)\right)$
32 fveq2 ${⊢}{x}={G}\left({X}\right)\to {H}\left({x}\right)={H}\left({G}\left({X}\right)\right)$
33 31 32 eqeq12d ${⊢}{x}={G}\left({X}\right)\to \left({F}\left({x}\right)={H}\left({x}\right)↔{F}\left({G}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)\right)$
34 33 rspcva ${⊢}\left({G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to {F}\left({G}\left({X}\right)\right)={H}\left({G}\left({X}\right)\right)$
35 34 eqcomd ${⊢}\left({G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)$
36 35 ex ${⊢}{G}\left({X}\right)\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\to \left(\forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)\right)$
37 30 36 syl6 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\right)\to \left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\to \left(\forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)\right)\right)$
38 37 com23 ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\right)\to \left(\forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\to \left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)\right)\right)$
39 38 3impia ${⊢}\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to \left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)\right)$
40 39 impcom ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to {H}\left({G}\left({X}\right)\right)={F}\left({G}\left({X}\right)\right)$
41 10 14 40 3eqtrrd ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to {F}\left({G}\left({X}\right)\right)=\left({H}\circ {K}\right)\left({X}\right)$
42 5 41 eqtrd ${⊢}\left(\left({G}Fn{A}\wedge {K}Fn{B}\right)\wedge \left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)$
43 42 ex ${⊢}\left({G}Fn{A}\wedge {K}Fn{B}\right)\to \left(\left({X}\in \left({A}\cap {B}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {x}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={H}\left({x}\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)\right)$