Metamath Proof Explorer

Theorem cycpm2tr

Description: A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses cycpm2.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
cycpm2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpm2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
cycpm2.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
cycpm2.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
cycpm2tr.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion cycpm2tr ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝑇 ‘ { 𝐼 , 𝐽 } ) )

Proof

Step Hyp Ref Expression
1 cycpm2.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 cycpm2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 cycpm2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
4 cycpm2.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
5 cycpm2.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
6 cycpm2tr.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
7 partfun ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝐼 , 𝐽 } , ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) , 𝑥 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ↦ 𝑥 ) )
8 7 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝐼 , 𝐽 } , ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) , 𝑥 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ↦ 𝑥 ) ) )
9 cshw1s2 ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ) → ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) = ⟨“ 𝐽 𝐼 ”⟩ )
10 3 4 9 syl2anc ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) = ⟨“ 𝐽 𝐼 ”⟩ )
11 10 coeq1d ⊢ ( 𝜑 → ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) = ( ⟨“ 𝐽 𝐼 ”⟩ ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) )
12 0nn0 ⊢ 0 ∈ ℕ0
13 12 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
14 1nn0 ⊢ 1 ∈ ℕ0
15 14 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
16 0ne1 ⊢ 0 ≠ 1
17 16 a1i ⊢ ( 𝜑 → 0 ≠ 1 )
18 13 4 15 3 17 3 4 5 coprprop ⊢ ( 𝜑 → ( { ⟨ 0 , 𝐽 ⟩ , ⟨ 1 , 𝐼 ⟩ } ∘ { ⟨ 𝐼 , 0 ⟩ , ⟨ 𝐽 , 1 ⟩ } ) = { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } )
19 s2prop ⊢ ( ( 𝐽 ∈ 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ⟨“ 𝐽 𝐼 ”⟩ = { ⟨ 0 , 𝐽 ⟩ , ⟨ 1 , 𝐼 ⟩ } )
20 4 3 19 syl2anc ⊢ ( 𝜑 → ⟨“ 𝐽 𝐼 ”⟩ = { ⟨ 0 , 𝐽 ⟩ , ⟨ 1 , 𝐼 ⟩ } )
21 s2prop ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ) → ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } )
22 3 4 21 syl2anc ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } )
23 22 cnveqd ⊢ ( 𝜑 → ◡ ⟨“ 𝐼 𝐽 ”⟩ = ◡ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } )
24 cnvprop ⊢ ( ( ( 0 ∈ ℕ0 ∧ 𝐼 ∈ 𝐷 ) ∧ ( 1 ∈ ℕ0 ∧ 𝐽 ∈ 𝐷 ) ) → ◡ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } = { ⟨ 𝐼 , 0 ⟩ , ⟨ 𝐽 , 1 ⟩ } )
25 13 3 15 4 24 syl22anc ⊢ ( 𝜑 → ◡ { ⟨ 0 , 𝐼 ⟩ , ⟨ 1 , 𝐽 ⟩ } = { ⟨ 𝐼 , 0 ⟩ , ⟨ 𝐽 , 1 ⟩ } )
26 23 25 eqtrd ⊢ ( 𝜑 → ◡ ⟨“ 𝐼 𝐽 ”⟩ = { ⟨ 𝐼 , 0 ⟩ , ⟨ 𝐽 , 1 ⟩ } )
27 20 26 coeq12d ⊢ ( 𝜑 → ( ⟨“ 𝐽 𝐼 ”⟩ ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) = ( { ⟨ 0 , 𝐽 ⟩ , ⟨ 1 , 𝐼 ⟩ } ∘ { ⟨ 𝐼 , 0 ⟩ , ⟨ 𝐽 , 1 ⟩ } ) )
28 3 4 4 3 5 mptprop ⊢ ( 𝜑 → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } = ( 𝑥 ∈ { 𝐼 , 𝐽 } ↦ if ( 𝑥 = 𝐼 , 𝐽 , 𝐼 ) ) )
29 3 4 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝐷 )
30 df-ss ⊢ ( { 𝐼 , 𝐽 } ⊆ 𝐷 ↔ ( { 𝐼 , 𝐽 } ∩ 𝐷 ) = { 𝐼 , 𝐽 } )
31 29 30 sylib ⊢ ( 𝜑 → ( { 𝐼 , 𝐽 } ∩ 𝐷 ) = { 𝐼 , 𝐽 } )
32 incom ⊢ ( { 𝐼 , 𝐽 } ∩ 𝐷 ) = ( 𝐷 ∩ { 𝐼 , 𝐽 } )
33 31 32 eqtr3di ⊢ ( 𝜑 → { 𝐼 , 𝐽 } = ( 𝐷 ∩ { 𝐼 , 𝐽 } ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → 𝑥 = 𝐼 )
35 34 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → { 𝑥 } = { 𝐼 } )
36 35 difeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) = ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) )
37 36 unieqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) = ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) )
38 difprsn1 ⊢ ( 𝐼 ≠ 𝐽 → ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) = { 𝐽 } )
39 38 unieqd ⊢ ( 𝐼 ≠ 𝐽 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) = ∪ { 𝐽 } )
40 5 39 syl ⊢ ( 𝜑 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) = ∪ { 𝐽 } )
41 unisng ⊢ ( 𝐽 ∈ 𝐷 → ∪ { 𝐽 } = 𝐽 )
42 4 41 syl ⊢ ( 𝜑 → ∪ { 𝐽 } = 𝐽 )
43 40 42 eqtrd ⊢ ( 𝜑 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) = 𝐽 )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐼 } ) = 𝐽 )
45 37 44 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ 𝑥 = 𝐼 ) → 𝐽 = ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) )
46 vex ⊢ 𝑥 ∈ V
47 46 elpr ⊢ ( 𝑥 ∈ { 𝐼 , 𝐽 } ↔ ( 𝑥 = 𝐼 ∨ 𝑥 = 𝐽 ) )
48 df-or ⊢ ( ( 𝑥 = 𝐼 ∨ 𝑥 = 𝐽 ) ↔ ( ¬ 𝑥 = 𝐼 → 𝑥 = 𝐽 ) )
49 47 48 sylbb ⊢ ( 𝑥 ∈ { 𝐼 , 𝐽 } → ( ¬ 𝑥 = 𝐼 → 𝑥 = 𝐽 ) )
50 49 imp ⊢ ( ( 𝑥 ∈ { 𝐼 , 𝐽 } ∧ ¬ 𝑥 = 𝐼 ) → 𝑥 = 𝐽 )
51 50 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → 𝑥 = 𝐽 )
52 51 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → { 𝑥 } = { 𝐽 } )
53 52 difeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) = ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) )
54 53 unieqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) = ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) )
55 difprsn2 ⊢ ( 𝐼 ≠ 𝐽 → ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) = { 𝐼 } )
56 55 unieqd ⊢ ( 𝐼 ≠ 𝐽 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) = ∪ { 𝐼 } )
57 5 56 syl ⊢ ( 𝜑 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) = ∪ { 𝐼 } )
58 unisng ⊢ ( 𝐼 ∈ 𝐷 → ∪ { 𝐼 } = 𝐼 )
59 3 58 syl ⊢ ( 𝜑 → ∪ { 𝐼 } = 𝐼 )
60 57 59 eqtrd ⊢ ( 𝜑 → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) = 𝐼 )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → ∪ ( { 𝐼 , 𝐽 } ∖ { 𝐽 } ) = 𝐼 )
62 54 61 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) ∧ ¬ 𝑥 = 𝐼 ) → 𝐼 = ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) )
63 45 62 ifeqda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝐼 , 𝐽 } ) → if ( 𝑥 = 𝐼 , 𝐽 , 𝐼 ) = ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) )
64 33 63 mpteq12dva ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝐼 , 𝐽 } ↦ if ( 𝑥 = 𝐼 , 𝐽 , 𝐼 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) )
65 28 64 eqtr2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) = { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } )
66 18 27 65 3eqtr4d ⊢ ( 𝜑 → ( ⟨“ 𝐽 𝐼 ”⟩ ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) )
67 11 66 eqtrd ⊢ ( 𝜑 → ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) )
68 3 4 s2rn ⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )
69 68 difeq2d ⊢ ( 𝜑 → ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝐷 ∖ { 𝐼 , 𝐽 } ) )
70 69 reseq2d ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( I ↾ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ) )
71 mptresid ⊢ ( I ↾ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ↦ 𝑥 )
72 70 71 eqtrdi ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ↦ 𝑥 ) )
73 67 72 uneq12d ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ∪ ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝐼 , 𝐽 } ) ↦ ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝐼 , 𝐽 } ) ↦ 𝑥 ) ) )
74 uncom ⊢ ( ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ∪ ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ) = ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ∪ ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) )
75 74 a1i ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ∪ ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ) = ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ∪ ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ) )
76 8 73 75 3eqtr2rd ⊢ ( 𝜑 → ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ∪ ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝐼 , 𝐽 } , ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) , 𝑥 ) ) )
77 3 4 s2cld ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
78 3 4 5 s2f1 ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
79 1 2 77 78 tocycfv ⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝐼 𝐽 ”⟩ ) ) ∪ ( ( ⟨“ 𝐼 𝐽 ”⟩ cyclShift 1 ) ∘ ◡ ⟨“ 𝐼 𝐽 ”⟩ ) ) )
80 pr2nelem ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽 ) → { 𝐼 , 𝐽 } ≈ 2o )
81 3 4 5 80 syl3anc ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ≈ 2o )
82 6 pmtrval ⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝐼 , 𝐽 } , ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) , 𝑥 ) ) )
83 2 29 81 82 syl3anc ⊢ ( 𝜑 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝐼 , 𝐽 } , ∪ ( { 𝐼 , 𝐽 } ∖ { 𝑥 } ) , 𝑥 ) ) )
84 76 79 83 3eqtr4d ⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝑇 ‘ { 𝐼 , 𝐽 } ) )