pmtr3ncomlem2

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

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 \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (G \circ F) (X) \neq (F \circ G) (X)$
5		fveq1	$⊢ G \circ F = F \circ G \to (G \circ F) (X) = (F \circ G) (X)$
6	5	necon3i	$⊢ (G \circ F) (X) \neq (F \circ G) (X) \to G \circ F \neq F \circ G$
7	4 6	syl	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to G \circ F \neq F \circ G$

Metamath Proof Explorer