Theorem pmtr3ncomlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		pmtr3ncom.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2		pmtr3ncom.f	⊢ 𝐹 = ( 𝑇 ‘ { 𝑋 , 𝑌 } )
3		pmtr3ncom.g	⊢ 𝐺 = ( 𝑇 ‘ { 𝑌 , 𝑍 } )
4		necom	⊢ ( 𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌 )
5	4	biimpi	⊢ ( 𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌 )
6	5	3ad2ant3	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ≠ 𝑌 )
7	6	3ad2ant3	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑍 ≠ 𝑌 )
8		simp1	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐷 ∈ 𝑉 )
9		simp1	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → 𝑋 ∈ 𝐷 )
10	9	3ad2ant2	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑋 ∈ 𝐷 )
11		simp2	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → 𝑌 ∈ 𝐷 )
12	11	3ad2ant2	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑌 ∈ 𝐷 )
13	10 12	prssd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑋 , 𝑌 } ⊆ 𝐷 )
14		simp1	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑋 ≠ 𝑌 )
15	14	3ad2ant3	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑋 ≠ 𝑌 )
16		pr2nelem	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
17	10 12 15 16	syl3anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
18	1	pmtrf	⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ⊆ 𝐷 ∧ { 𝑋 , 𝑌 } ≈ 2o ) → ( 𝑇 ‘ { 𝑋 , 𝑌 } ) : 𝐷 ⟶ 𝐷 )
19	8 13 17 18	syl3anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝑇 ‘ { 𝑋 , 𝑌 } ) : 𝐷 ⟶ 𝐷 )
20	2	feq1i	⊢ ( 𝐹 : 𝐷 ⟶ 𝐷 ↔ ( 𝑇 ‘ { 𝑋 , 𝑌 } ) : 𝐷 ⟶ 𝐷 )
21	19 20	sylibr	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐹 : 𝐷 ⟶ 𝐷 )
22	21	ffnd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐹 Fn 𝐷 )
23		fvco2	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )
24	22 10 23	syl2anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )
25	2	fveq1i	⊢ ( 𝐹 ‘ 𝑋 ) = ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 )
26	10 12 15	3jca	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) )
27	1	pmtrprfv	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )
28	8 26 27	syl2anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )
29	25 28	eqtrid	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
30	29	fveq2d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐺 ‘ 𝑌 ) )
31	3	fveq1i	⊢ ( 𝐺 ‘ 𝑌 ) = ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑌 )
32		simp3	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → 𝑍 ∈ 𝐷 )
33	32	3ad2ant2	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑍 ∈ 𝐷 )
34		simp3	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ≠ 𝑍 )
35	34	3ad2ant3	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑌 ≠ 𝑍 )
36	12 33 35	3jca	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑌 ≠ 𝑍 ) )
37	1	pmtrprfv	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑌 ) = 𝑍 )
38	8 36 37	syl2anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑌 ) = 𝑍 )
39	31 38	eqtrid	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ‘ 𝑌 ) = 𝑍 )
40	24 30 39	3eqtrd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) = 𝑍 )
41	11 32	prssd	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → { 𝑌 , 𝑍 } ⊆ 𝐷 )
42	41	3ad2ant2	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑌 , 𝑍 } ⊆ 𝐷 )
43		pr2nelem	⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑌 ≠ 𝑍 ) → { 𝑌 , 𝑍 } ≈ 2o )
44	12 33 35 43	syl3anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑌 , 𝑍 } ≈ 2o )
45	1	pmtrf	⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝑌 , 𝑍 } ⊆ 𝐷 ∧ { 𝑌 , 𝑍 } ≈ 2o ) → ( 𝑇 ‘ { 𝑌 , 𝑍 } ) : 𝐷 ⟶ 𝐷 )
46	3	feq1i	⊢ ( 𝐺 : 𝐷 ⟶ 𝐷 ↔ ( 𝑇 ‘ { 𝑌 , 𝑍 } ) : 𝐷 ⟶ 𝐷 )
47	45 46	sylibr	⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝑌 , 𝑍 } ⊆ 𝐷 ∧ { 𝑌 , 𝑍 } ≈ 2o ) → 𝐺 : 𝐷 ⟶ 𝐷 )
48	8 42 44 47	syl3anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐺 : 𝐷 ⟶ 𝐷 )
49	48	ffnd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐺 Fn 𝐷 )
50		fvco2	⊢ ( ( 𝐺 Fn 𝐷 ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
51	49 10 50	syl2anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
52	3	fveq1i	⊢ ( 𝐺 ‘ 𝑋 ) = ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑋 )
53		id	⊢ ( 𝐷 ∈ 𝑉 → 𝐷 ∈ 𝑉 )
54		3anrot	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) )
55	54	biimpi	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) )
56		3anrot	⊢ ( ( 𝑌 ≠ 𝑍 ∧ 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) ↔ ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ∧ 𝑌 ≠ 𝑍 ) )
57		necom	⊢ ( 𝑌 ≠ 𝑋 ↔ 𝑋 ≠ 𝑌 )
58		necom	⊢ ( 𝑍 ≠ 𝑋 ↔ 𝑋 ≠ 𝑍 )
59		biid	⊢ ( 𝑌 ≠ 𝑍 ↔ 𝑌 ≠ 𝑍 )
60	57 58 59	3anbi123i	⊢ ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ∧ 𝑌 ≠ 𝑍 ) ↔ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) )
61	56 60	sylbbr	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 ≠ 𝑍 ∧ 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) )
62	1	pmtrprfv3	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) ∧ ( 𝑌 ≠ 𝑍 ∧ 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑋 ) = 𝑋 )
63	53 55 61 62	syl3an	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑍 } ) ‘ 𝑋 ) = 𝑋 )
64	52 63	eqtrid	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐺 ‘ 𝑋 ) = 𝑋 )
65	64	fveq2d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
66	51 65 29	3eqtrd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = 𝑌 )
67	7 40 66	3netr4d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) ≠ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) )