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 ⊢ ( ( 𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃 ) → ( ( 𝑋 ∈ 𝐼 ∧ ( 𝐺 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ∧ ∀ 𝑛 ∈ 𝐼 ( 𝐹 ‘ 𝑛 ) = ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐻 ∘ 𝐾 ) ‘ 𝑋 ) ) )