# 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 𝑆 = ( SymGrp ‘ 𝑁 )
gsmsymgrfix.b 𝐵 = ( Base ‘ 𝑆 )
gsmsymgreq.z 𝑍 = ( SymGrp ‘ 𝑀 )
gsmsymgreq.p 𝑃 = ( Base ‘ 𝑍 )
gsmsymgreq.i 𝐼 = ( 𝑁𝑀 )
Assertion fvcosymgeq ( ( 𝐺𝐵𝐾𝑃 ) → ( ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( ( 𝐻𝐾 ) ‘ 𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s 𝑆 = ( SymGrp ‘ 𝑁 )
2 gsmsymgrfix.b 𝐵 = ( Base ‘ 𝑆 )
3 gsmsymgreq.z 𝑍 = ( SymGrp ‘ 𝑀 )
4 gsmsymgreq.p 𝑃 = ( Base ‘ 𝑍 )
5 gsmsymgreq.i 𝐼 = ( 𝑁𝑀 )
6 1 2 symgbasf ( 𝐺𝐵𝐺 : 𝑁𝑁 )
7 6 ffnd ( 𝐺𝐵𝐺 Fn 𝑁 )
8 3 4 symgbasf ( 𝐾𝑃𝐾 : 𝑀𝑀 )
9 8 ffnd ( 𝐾𝑃𝐾 Fn 𝑀 )
10 7 9 anim12i ( ( 𝐺𝐵𝐾𝑃 ) → ( 𝐺 Fn 𝑁𝐾 Fn 𝑀 ) )
11 10 adantr ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → ( 𝐺 Fn 𝑁𝐾 Fn 𝑀 ) )
12 5 eleq2i ( 𝑋𝐼𝑋 ∈ ( 𝑁𝑀 ) )
13 12 biimpi ( 𝑋𝐼𝑋 ∈ ( 𝑁𝑀 ) )
14 13 3ad2ant1 ( ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) → 𝑋 ∈ ( 𝑁𝑀 ) )
15 14 adantl ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → 𝑋 ∈ ( 𝑁𝑀 ) )
16 simpr2 ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → ( 𝐺𝑋 ) = ( 𝐾𝑋 ) )
17 1 2 symgbasf1o ( 𝐺𝐵𝐺 : 𝑁1-1-onto𝑁 )
18 dff1o5 ( 𝐺 : 𝑁1-1-onto𝑁 ↔ ( 𝐺 : 𝑁1-1𝑁 ∧ ran 𝐺 = 𝑁 ) )
19 eqcom ( ran 𝐺 = 𝑁𝑁 = ran 𝐺 )
20 19 biimpi ( ran 𝐺 = 𝑁𝑁 = ran 𝐺 )
21 18 20 simplbiim ( 𝐺 : 𝑁1-1-onto𝑁𝑁 = ran 𝐺 )
22 17 21 syl ( 𝐺𝐵𝑁 = ran 𝐺 )
23 3 4 symgbasf1o ( 𝐾𝑃𝐾 : 𝑀1-1-onto𝑀 )
24 dff1o5 ( 𝐾 : 𝑀1-1-onto𝑀 ↔ ( 𝐾 : 𝑀1-1𝑀 ∧ ran 𝐾 = 𝑀 ) )
25 eqcom ( ran 𝐾 = 𝑀𝑀 = ran 𝐾 )
26 25 biimpi ( ran 𝐾 = 𝑀𝑀 = ran 𝐾 )
27 24 26 simplbiim ( 𝐾 : 𝑀1-1-onto𝑀𝑀 = ran 𝐾 )
28 23 27 syl ( 𝐾𝑃𝑀 = ran 𝐾 )
29 22 28 ineqan12d ( ( 𝐺𝐵𝐾𝑃 ) → ( 𝑁𝑀 ) = ( ran 𝐺 ∩ ran 𝐾 ) )
30 5 29 syl5eq ( ( 𝐺𝐵𝐾𝑃 ) → 𝐼 = ( ran 𝐺 ∩ ran 𝐾 ) )
31 30 raleqdv ( ( 𝐺𝐵𝐾𝑃 ) → ( ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ↔ ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) )
32 31 biimpcd ( ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) → ( ( 𝐺𝐵𝐾𝑃 ) → ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) )
33 32 3ad2ant3 ( ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) → ( ( 𝐺𝐵𝐾𝑃 ) → ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) )
34 33 impcom ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) )
35 15 16 34 3jca ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → ( 𝑋 ∈ ( 𝑁𝑀 ) ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) )
36 fvcofneq ( ( 𝐺 Fn 𝑁𝐾 Fn 𝑀 ) → ( ( 𝑋 ∈ ( 𝑁𝑀 ) ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛 ∈ ( ran 𝐺 ∩ ran 𝐾 ) ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( ( 𝐻𝐾 ) ‘ 𝑋 ) ) )
37 11 35 36 sylc ( ( ( 𝐺𝐵𝐾𝑃 ) ∧ ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( ( 𝐻𝐾 ) ‘ 𝑋 ) )
38 37 ex ( ( 𝐺𝐵𝐾𝑃 ) → ( ( 𝑋𝐼 ∧ ( 𝐺𝑋 ) = ( 𝐾𝑋 ) ∧ ∀ 𝑛𝐼 ( 𝐹𝑛 ) = ( 𝐻𝑛 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( ( 𝐻𝐾 ) ‘ 𝑋 ) ) )