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 = ( SymGrp ` N )
gsmsymgrfix.b 
|- B = ( Base ` S )
gsmsymgreq.z 
|- Z = ( SymGrp ` M )
gsmsymgreq.p 
|- P = ( Base ` Z )
gsmsymgreq.i 
|- I = ( N i^i M )
Assertion fvcosymgeq 
|- ( ( G e. B /\ K e. P ) -> ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s 
 |-  S = ( SymGrp ` N )
2 gsmsymgrfix.b 
 |-  B = ( Base ` S )
3 gsmsymgreq.z 
 |-  Z = ( SymGrp ` M )
4 gsmsymgreq.p 
 |-  P = ( Base ` Z )
5 gsmsymgreq.i 
 |-  I = ( N i^i M )
6 1 2 symgbasf 
 |-  ( G e. B -> G : N --> N )
7 6 ffnd 
 |-  ( G e. B -> G Fn N )
8 3 4 symgbasf 
 |-  ( K e. P -> K : M --> M )
9 8 ffnd 
 |-  ( K e. P -> K Fn M )
10 7 9 anim12i 
 |-  ( ( G e. B /\ K e. P ) -> ( G Fn N /\ K Fn M ) )
11 10 adantr 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> ( G Fn N /\ K Fn M ) )
12 5 eleq2i 
 |-  ( X e. I <-> X e. ( N i^i M ) )
13 12 biimpi 
 |-  ( X e. I -> X e. ( N i^i M ) )
14 13 3ad2ant1 
 |-  ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> X e. ( N i^i M ) )
15 14 adantl 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> X e. ( N i^i M ) )
16 simpr2 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> ( G ` X ) = ( K ` X ) )
17 1 2 symgbasf1o 
 |-  ( G e. B -> G : N -1-1-onto-> N )
18 dff1o5 
 |-  ( G : N -1-1-onto-> N <-> ( G : N -1-1-> N /\ ran G = N ) )
19 eqcom 
 |-  ( ran G = N <-> N = ran G )
20 19 biimpi 
 |-  ( ran G = N -> N = ran G )
21 18 20 simplbiim 
 |-  ( G : N -1-1-onto-> N -> N = ran G )
22 17 21 syl 
 |-  ( G e. B -> N = ran G )
23 3 4 symgbasf1o 
 |-  ( K e. P -> K : M -1-1-onto-> M )
24 dff1o5 
 |-  ( K : M -1-1-onto-> M <-> ( K : M -1-1-> M /\ ran K = M ) )
25 eqcom 
 |-  ( ran K = M <-> M = ran K )
26 25 biimpi 
 |-  ( ran K = M -> M = ran K )
27 24 26 simplbiim 
 |-  ( K : M -1-1-onto-> M -> M = ran K )
28 23 27 syl 
 |-  ( K e. P -> M = ran K )
29 22 28 ineqan12d 
 |-  ( ( G e. B /\ K e. P ) -> ( N i^i M ) = ( ran G i^i ran K ) )
30 5 29 syl5eq 
 |-  ( ( G e. B /\ K e. P ) -> I = ( ran G i^i ran K ) )
31 30 raleqdv 
 |-  ( ( G e. B /\ K e. P ) -> ( A. n e. I ( F ` n ) = ( H ` n ) <-> A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) ) )
32 31 biimpcd 
 |-  ( A. n e. I ( F ` n ) = ( H ` n ) -> ( ( G e. B /\ K e. P ) -> A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) ) )
33 32 3ad2ant3 
 |-  ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> ( ( G e. B /\ K e. P ) -> A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) ) )
34 33 impcom 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) )
35 15 16 34 3jca 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> ( X e. ( N i^i M ) /\ ( G ` X ) = ( K ` X ) /\ A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) ) )
36 fvcofneq 
 |-  ( ( G Fn N /\ K Fn M ) -> ( ( X e. ( N i^i M ) /\ ( G ` X ) = ( K ` X ) /\ A. n e. ( ran G i^i ran K ) ( F ` n ) = ( H ` n ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )
37 11 35 36 sylc 
 |-  ( ( ( G e. B /\ K e. P ) /\ ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) )
38 37 ex 
 |-  ( ( G e. B /\ K e. P ) -> ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )