# Metamath Proof Explorer

## Theorem fvcosymgeq

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

Ref Expression
Hypotheses gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
Assertion fvcosymgeq ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to \left(\left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\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 gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
2 gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
4 gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
5 gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
6 1 2 symgbasf ${⊢}{G}\in {B}\to {G}:{N}⟶{N}$
7 6 ffnd ${⊢}{G}\in {B}\to {G}Fn{N}$
8 3 4 symgbasf ${⊢}{K}\in {P}\to {K}:{M}⟶{M}$
9 8 ffnd ${⊢}{K}\in {P}\to {K}Fn{M}$
10 7 9 anim12i ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to \left({G}Fn{N}\wedge {K}Fn{M}\right)$
11 10 adantr ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to \left({G}Fn{N}\wedge {K}Fn{M}\right)$
12 5 eleq2i ${⊢}{X}\in {I}↔{X}\in \left({N}\cap {M}\right)$
13 12 biimpi ${⊢}{X}\in {I}\to {X}\in \left({N}\cap {M}\right)$
14 13 3ad2ant1 ${⊢}\left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\to {X}\in \left({N}\cap {M}\right)$
15 14 adantl ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to {X}\in \left({N}\cap {M}\right)$
16 simpr2 ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to {G}\left({X}\right)={K}\left({X}\right)$
17 1 2 symgbasf1o ${⊢}{G}\in {B}\to {G}:{N}\underset{1-1 onto}{⟶}{N}$
18 dff1o5 ${⊢}{G}:{N}\underset{1-1 onto}{⟶}{N}↔\left({G}:{N}\underset{1-1}{⟶}{N}\wedge \mathrm{ran}{G}={N}\right)$
19 eqcom ${⊢}\mathrm{ran}{G}={N}↔{N}=\mathrm{ran}{G}$
20 19 biimpi ${⊢}\mathrm{ran}{G}={N}\to {N}=\mathrm{ran}{G}$
21 18 20 simplbiim ${⊢}{G}:{N}\underset{1-1 onto}{⟶}{N}\to {N}=\mathrm{ran}{G}$
22 17 21 syl ${⊢}{G}\in {B}\to {N}=\mathrm{ran}{G}$
23 3 4 symgbasf1o ${⊢}{K}\in {P}\to {K}:{M}\underset{1-1 onto}{⟶}{M}$
24 dff1o5 ${⊢}{K}:{M}\underset{1-1 onto}{⟶}{M}↔\left({K}:{M}\underset{1-1}{⟶}{M}\wedge \mathrm{ran}{K}={M}\right)$
25 eqcom ${⊢}\mathrm{ran}{K}={M}↔{M}=\mathrm{ran}{K}$
26 25 biimpi ${⊢}\mathrm{ran}{K}={M}\to {M}=\mathrm{ran}{K}$
27 24 26 simplbiim ${⊢}{K}:{M}\underset{1-1 onto}{⟶}{M}\to {M}=\mathrm{ran}{K}$
28 23 27 syl ${⊢}{K}\in {P}\to {M}=\mathrm{ran}{K}$
29 22 28 ineqan12d ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to {N}\cap {M}=\mathrm{ran}{G}\cap \mathrm{ran}{K}$
30 5 29 syl5eq ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to {I}=\mathrm{ran}{G}\cap \mathrm{ran}{K}$
31 30 raleqdv ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)↔\forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)$
32 31 biimpcd ${⊢}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\to \left(\left({G}\in {B}\wedge {K}\in {P}\right)\to \forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)$
33 32 3ad2ant3 ${⊢}\left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\to \left(\left({G}\in {B}\wedge {K}\in {P}\right)\to \forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)$
34 33 impcom ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to \forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)$
35 15 16 34 3jca ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to \left({X}\in \left({N}\cap {M}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)$
36 fvcofneq ${⊢}\left({G}Fn{N}\wedge {K}Fn{M}\right)\to \left(\left({X}\in \left({N}\cap {M}\right)\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in \left(\mathrm{ran}{G}\cap \mathrm{ran}{K}\right)\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)\right)$
37 11 35 36 sylc ${⊢}\left(\left({G}\in {B}\wedge {K}\in {P}\right)\wedge \left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)$
38 37 ex ${⊢}\left({G}\in {B}\wedge {K}\in {P}\right)\to \left(\left({X}\in {I}\wedge {G}\left({X}\right)={K}\left({X}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)={H}\left({n}\right)\right)\to \left({F}\circ {G}\right)\left({X}\right)=\left({H}\circ {K}\right)\left({X}\right)\right)$