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 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) )