This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtr3ncomlem2

Description: Lemma 2 for pmtr3ncom . (Contributed by AV, 17-Mar-2018)

Ref Expression
Hypotheses pmtr3ncom.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtr3ncom.f ⊢ 𝐹 = ( 𝑇 ‘ { 𝑋 , 𝑌 } )
pmtr3ncom.g ⊢ 𝐺 = ( 𝑇 ‘ { 𝑌 , 𝑍 } )
Assertion pmtr3ncomlem2 ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ∘ 𝐹 ) ≠ ( 𝐹 ∘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pmtr3ncom.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtr3ncom.f ⊢ 𝐹 = ( 𝑇 ‘ { 𝑋 , 𝑌 } )
3 pmtr3ncom.g ⊢ 𝐺 = ( 𝑇 ‘ { 𝑌 , 𝑍 } )
4 1 2 3 pmtr3ncomlem1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) ≠ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) )
5 fveq1 ⊢ ( ( 𝐺 ∘ 𝐹 ) = ( 𝐹 ∘ 𝐺 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) )
6 5 necon3i ⊢ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) ≠ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) → ( 𝐺 ∘ 𝐹 ) ≠ ( 𝐹 ∘ 𝐺 ) )
7 4 6 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ∘ 𝐹 ) ≠ ( 𝐹 ∘ 𝐺 ) )