This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 enpr2 ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ≈ 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 enpr2 ⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ∧ 𝑌 ≠ 𝑍 ) → { 𝑌 , 𝑍 } ≈ 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 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑋 ) ≠ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) )