Theorem pmtr3ncomlem2

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

	Ref	Expression
Hypotheses	pmtr3ncom.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
	pmtr3ncom.f	$$⊢F=T\left(\left\{X,Y\right\}\right)$$
	pmtr3ncom.g	$$⊢G=T\left(\left\{Y,Z\right\}\right)$$
Assertion	pmtr3ncomlem2	$$⊢\left(D\in V\wedge \left(X\in D\wedge Y\in D\wedge Z\in D\right)\wedge \left(X\ne Y\wedge X\ne Z\wedge Y\ne Z\right)\right)\to G\circ F\ne F\circ G$$

Proof

Step	Hyp	Ref	Expression
1		pmtr3ncom.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
2		pmtr3ncom.f	$$⊢F=T\left(\left\{X,Y\right\}\right)$$
3		pmtr3ncom.g	$$⊢G=T\left(\left\{Y,Z\right\}\right)$$
4	1 2 3	pmtr3ncomlem1	$$⊢\left(D\in V\wedge \left(X\in D\wedge Y\in D\wedge Z\in D\right)\wedge \left(X\ne Y\wedge X\ne Z\wedge Y\ne Z\right)\right)\to \left(G\circ F\right)\left(X\right)\ne \left(F\circ G\right)\left(X\right)$$
5		fveq1	$$⊢G\circ F=F\circ G\to \left(G\circ F\right)\left(X\right)=\left(F\circ G\right)\left(X\right)$$
6	5	necon3i	$$⊢\left(G\circ F\right)\left(X\right)\ne \left(F\circ G\right)\left(X\right)\to G\circ F\ne F\circ G$$
7	4 6	syl	$$⊢\left(D\in V\wedge \left(X\in D\wedge Y\in D\wedge Z\in D\right)\wedge \left(X\ne Y\wedge X\ne Z\wedge Y\ne Z\right)\right)\to G\circ F\ne F\circ G$$