Metamath Proof Explorer

Theorem pmtrfconj

Description: Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r ⊢ 𝑅 = ran 𝑇
Assertion pmtrfconj ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∈ 𝑅 )

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtrrn.r ⊢ 𝑅 = ran 𝑇
3 1 2 pmtrfb ⊢ ( 𝐹 ∈ 𝑅 ↔ ( 𝐷 ∈ V ∧ 𝐹 : 𝐷 –1-1-onto→ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
4 3 simp1bi ⊢ ( 𝐹 ∈ 𝑅 → 𝐷 ∈ V )
5 4 adantr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → 𝐷 ∈ V )
6 simpr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
7 1 2 pmtrff1o ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
8 7 adantr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
9 f1oco ⊢ ( ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 ∧ 𝐹 : 𝐷 –1-1-onto→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 )
10 6 8 9 syl2anc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 )
11 f1ocnv ⊢ ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
12 11 adantl ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
13 f1oco ⊢ ( ( ( 𝐺 ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 ∧ ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) : 𝐷 –1-1-onto→ 𝐷 )
14 10 12 13 syl2anc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) : 𝐷 –1-1-onto→ 𝐷 )
15 f1of ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 : 𝐷 ⟶ 𝐷 )
16 7 15 syl ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 : 𝐷 ⟶ 𝐷 )
17 16 adantr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → 𝐹 : 𝐷 ⟶ 𝐷 )
18 f1omvdconj ⊢ ( ( 𝐹 : 𝐷 ⟶ 𝐷 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) = ( 𝐺 “ dom ( 𝐹 ∖ I ) ) )
19 17 6 18 syl2anc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) = ( 𝐺 “ dom ( 𝐹 ∖ I ) ) )
20 f1of1 ⊢ ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 → 𝐺 : 𝐷 –1-1→ 𝐷 )
21 20 adantl ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → 𝐺 : 𝐷 –1-1→ 𝐷 )
22 difss ⊢ ( 𝐹 ∖ I ) ⊆ 𝐹
23 dmss ⊢ ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
24 22 23 ax-mp ⊢ dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
25 24 17 fssdm ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( 𝐹 ∖ I ) ⊆ 𝐷 )
26 5 25 ssexd ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( 𝐹 ∖ I ) ∈ V )
27 f1imaeng ⊢ ( ( 𝐺 : 𝐷 –1-1→ 𝐷 ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ∈ V ) → ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ≈ dom ( 𝐹 ∖ I ) )
28 21 25 26 27 syl3anc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ≈ dom ( 𝐹 ∖ I ) )
29 19 28 eqbrtrd ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) ≈ dom ( 𝐹 ∖ I ) )
30 3 simp3bi ⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≈ 2o )
31 30 adantr ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( 𝐹 ∖ I ) ≈ 2o )
32 entr ⊢ ( ( dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) ≈ dom ( 𝐹 ∖ I ) ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) ≈ 2o )
33 29 31 32 syl2anc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) ≈ 2o )
34 1 2 pmtrfb ⊢ ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∈ 𝑅 ↔ ( 𝐷 ∈ V ∧ ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) : 𝐷 –1-1-onto→ 𝐷 ∧ dom ( ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∖ I ) ≈ 2o ) )
35 5 14 33 34 syl3anbrc ⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) ∘ ◡ 𝐺 ) ∈ 𝑅 )