Metamath Proof Explorer


Theorem pmtr3ncom

Description: Transpositions over sets with at least 3 elements are not commutative, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)

Ref Expression
Hypothesis pmtr3ncom.t 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtr3ncom ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) )

Proof

Step Hyp Ref Expression
1 pmtr3ncom.t 𝑇 = ( pmTrsp ‘ 𝐷 )
2 hashge3el3dif ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥𝐷𝑦𝐷𝑧𝐷 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) )
3 simprl ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → 𝐷𝑉 )
4 prssi ( ( 𝑥𝐷𝑦𝐷 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 )
5 4 adantr ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 )
6 5 ad2antrr ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑥 , 𝑦 } ⊆ 𝐷 )
7 simplll ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → 𝑥𝐷 )
8 simplr ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) → 𝑦𝐷 )
9 8 adantr ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → 𝑦𝐷 )
10 simpr1 ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → 𝑥𝑦 )
11 pr2nelem ( ( 𝑥𝐷𝑦𝐷𝑥𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o )
12 7 9 10 11 syl3anc ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → { 𝑥 , 𝑦 } ≈ 2o )
13 12 adantr ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑥 , 𝑦 } ≈ 2o )
14 eqid ran 𝑇 = ran 𝑇
15 1 14 pmtrrn ( ( 𝐷𝑉 ∧ { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ { 𝑥 , 𝑦 } ≈ 2o ) → ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 )
16 3 6 13 15 syl3anc ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 )
17 prssi ( ( 𝑦𝐷𝑧𝐷 ) → { 𝑦 , 𝑧 } ⊆ 𝐷 )
18 17 ad5ant23 ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑦 , 𝑧 } ⊆ 𝐷 )
19 simplr ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → 𝑧𝐷 )
20 simpr3 ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → 𝑦𝑧 )
21 pr2nelem ( ( 𝑦𝐷𝑧𝐷𝑦𝑧 ) → { 𝑦 , 𝑧 } ≈ 2o )
22 9 19 20 21 syl3anc ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → { 𝑦 , 𝑧 } ≈ 2o )
23 22 adantr ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑦 , 𝑧 } ≈ 2o )
24 1 14 pmtrrn ( ( 𝐷𝑉 ∧ { 𝑦 , 𝑧 } ⊆ 𝐷 ∧ { 𝑦 , 𝑧 } ≈ 2o ) → ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 )
25 3 18 23 24 syl3anc ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 )
26 df-3an ( ( 𝑥𝐷𝑦𝐷𝑧𝐷 ) ↔ ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) )
27 26 biimpri ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) → ( 𝑥𝐷𝑦𝐷𝑧𝐷 ) )
28 27 ad2antrr ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑥𝐷𝑦𝐷𝑧𝐷 ) )
29 simplr ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) )
30 eqid ( 𝑇 ‘ { 𝑥 , 𝑦 } ) = ( 𝑇 ‘ { 𝑥 , 𝑦 } )
31 eqid ( 𝑇 ‘ { 𝑦 , 𝑧 } ) = ( 𝑇 ‘ { 𝑦 , 𝑧 } )
32 1 30 31 pmtr3ncomlem2 ( ( 𝐷𝑉 ∧ ( 𝑥𝐷𝑦𝐷𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) → ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) )
33 3 28 29 32 syl3anc ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) )
34 coeq2 ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( 𝑔𝑓 ) = ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )
35 coeq1 ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( 𝑓𝑔 ) = ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) )
36 34 35 neeq12d ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) ↔ ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) )
37 coeq1 ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) = ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) )
38 coeq2 ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) = ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) )
39 37 38 neeq12d ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ↔ ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) )
40 36 39 rspc2ev ( ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 ∧ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 ∧ ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) )
41 16 25 33 40 syl3anc ( ( ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ) ∧ ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) )
42 41 exp31 ( ( ( 𝑥𝐷𝑦𝐷 ) ∧ 𝑧𝐷 ) → ( ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) → ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) ) ) )
43 42 rexlimdva ( ( 𝑥𝐷𝑦𝐷 ) → ( ∃ 𝑧𝐷 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) → ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) ) ) )
44 43 rexlimivv ( ∃ 𝑥𝐷𝑦𝐷𝑧𝐷 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) → ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) ) )
45 2 44 mpcom ( ( 𝐷𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇𝑔 ∈ ran 𝑇 ( 𝑔𝑓 ) ≠ ( 𝑓𝑔 ) )