Theorem pmtr3ncomlem2

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

	Ref	Expression
Hypotheses	pmtr3ncom.t	|- T = ( pmTrsp ` D )
	pmtr3ncom.f	|- F = ( T ` { X , Y } )
	pmtr3ncom.g	|- G = ( T ` { Y , Z } )
Assertion	pmtr3ncomlem2	|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G o. F ) =/= ( F o. G ) )

Proof

Step	Hyp	Ref	Expression
1		pmtr3ncom.t	|- T = ( pmTrsp ` D )
2		pmtr3ncom.f	|- F = ( T ` { X , Y } )
3		pmtr3ncom.g	|- G = ( T ` { Y , Z } )
4	1 2 3	pmtr3ncomlem1	|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( G o. F ) ` X ) =/= ( ( F o. G ) ` X ) )
5		fveq1	|- ( ( G o. F ) = ( F o. G ) -> ( ( G o. F ) ` X ) = ( ( F o. G ) ` X ) )
6	5	necon3i	|- ( ( ( G o. F ) ` X ) =/= ( ( F o. G ) ` X ) -> ( G o. F ) =/= ( F o. G ) )
7	4 6	syl	|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G o. F ) =/= ( F o. G ) )