Metamath Proof Explorer

Theorem pmtr3ncomlem1

Description: Lemma 1 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 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 ) )

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 necom 
 |-  ( Y =/= Z <-> Z =/= Y )
5 4 biimpi 
 |-  ( Y =/= Z -> Z =/= Y )
6 5 3ad2ant3 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Z =/= Y )
7 6 3ad2ant3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z =/= Y )
8 simp1 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> D e. V )
9 simp1 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> X e. D )
10 9 3ad2ant2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> X e. D )
11 simp2 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> Y e. D )
12 11 3ad2ant2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Y e. D )
13 10 12 prssd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } C_ D )
14 simp1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> X =/= Y )
15 14 3ad2ant3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> X =/= Y )
16 pr2nelem 
 |-  ( ( X e. D /\ Y e. D /\ X =/= Y ) -> { X , Y } ~~ 2o )
17 10 12 15 16 syl3anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } ~~ 2o )
18 1 pmtrf 
 |-  ( ( D e. V /\ { X , Y } C_ D /\ { X , Y } ~~ 2o ) -> ( T ` { X , Y } ) : D --> D )
19 8 13 17 18 syl3anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( T ` { X , Y } ) : D --> D )
20 2 feq1i 
 |-  ( F : D --> D <-> ( T ` { X , Y } ) : D --> D )
21 19 20 sylibr 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> F : D --> D )
22 21 ffnd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> F Fn D )
23 fvco2 
 |-  ( ( F Fn D /\ X e. D ) -> ( ( G o. F ) ` X ) = ( G ` ( F ` X ) ) )
24 22 10 23 syl2anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( G o. F ) ` X ) = ( G ` ( F ` X ) ) )
25 2 fveq1i 
 |-  ( F ` X ) = ( ( T ` { X , Y } ) ` X )
26 10 12 15 3jca 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( X e. D /\ Y e. D /\ X =/= Y ) )
27 1 pmtrprfv 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` X ) = Y )
28 8 26 27 syl2anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` X ) = Y )
29 25 28 syl5eq 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( F ` X ) = Y )
30 29 fveq2d 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G ` ( F ` X ) ) = ( G ` Y ) )
31 3 fveq1i 
 |-  ( G ` Y ) = ( ( T ` { Y , Z } ) ` Y )
32 simp3 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> Z e. D )
33 32 3ad2ant2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z e. D )
34 simp3 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Y =/= Z )
35 34 3ad2ant3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Y =/= Z )
36 12 33 35 3jca 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( Y e. D /\ Z e. D /\ Y =/= Z ) )
37 1 pmtrprfv 
 |-  ( ( D e. V /\ ( Y e. D /\ Z e. D /\ Y =/= Z ) ) -> ( ( T ` { Y , Z } ) ` Y ) = Z )
38 8 36 37 syl2anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { Y , Z } ) ` Y ) = Z )
39 31 38 syl5eq 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G ` Y ) = Z )
40 24 30 39 3eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( G o. F ) ` X ) = Z )
41 11 32 prssd 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> { Y , Z } C_ D )
42 41 3ad2ant2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { Y , Z } C_ D )
43 pr2nelem 
 |-  ( ( Y e. D /\ Z e. D /\ Y =/= Z ) -> { Y , Z } ~~ 2o )
44 12 33 35 43 syl3anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { Y , Z } ~~ 2o )
45 1 pmtrf 
 |-  ( ( D e. V /\ { Y , Z } C_ D /\ { Y , Z } ~~ 2o ) -> ( T ` { Y , Z } ) : D --> D )
46 3 feq1i 
 |-  ( G : D --> D <-> ( T ` { Y , Z } ) : D --> D )
47 45 46 sylibr 
 |-  ( ( D e. V /\ { Y , Z } C_ D /\ { Y , Z } ~~ 2o ) -> G : D --> D )
48 8 42 44 47 syl3anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> G : D --> D )
49 48 ffnd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> G Fn D )
50 fvco2 
 |-  ( ( G Fn D /\ X e. D ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
51 49 10 50 syl2anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
52 3 fveq1i 
 |-  ( G ` X ) = ( ( T ` { Y , Z } ) ` X )
53 id 
 |-  ( D e. V -> D e. V )
54 3anrot 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) <-> ( Y e. D /\ Z e. D /\ X e. D ) )
55 54 biimpi 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> ( Y e. D /\ Z e. D /\ X e. D ) )
56 3anrot 
 |-  ( ( Y =/= Z /\ Y =/= X /\ Z =/= X ) <-> ( Y =/= X /\ Z =/= X /\ Y =/= Z ) )
57 necom 
 |-  ( Y =/= X <-> X =/= Y )
58 necom 
 |-  ( Z =/= X <-> X =/= Z )
59 biid 
 |-  ( Y =/= Z <-> Y =/= Z )
60 57 58 59 3anbi123i 
 |-  ( ( Y =/= X /\ Z =/= X /\ Y =/= Z ) <-> ( X =/= Y /\ X =/= Z /\ Y =/= Z ) )
61 56 60 sylbbr 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( Y =/= Z /\ Y =/= X /\ Z =/= X ) )
62 1 pmtrprfv3 
 |-  ( ( D e. V /\ ( Y e. D /\ Z e. D /\ X e. D ) /\ ( Y =/= Z /\ Y =/= X /\ Z =/= X ) ) -> ( ( T ` { Y , Z } ) ` X ) = X )
63 53 55 61 62 syl3an 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { Y , Z } ) ` X ) = X )
64 52 63 syl5eq 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G ` X ) = X )
65 64 fveq2d 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( F ` ( G ` X ) ) = ( F ` X ) )
66 51 65 29 3eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( F o. G ) ` X ) = Y )
67 7 40 66 3netr4d 
 |-  ( ( 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 ) )