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	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ∘ 𝐹 ) ≠ ( 𝐹 ∘ 𝐺 ) )