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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> X e. ( N i^i M ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) ) )`