Metamath Proof Explorer

Theorem cgraswap

Description: Swap rays in a congruence relation. Theorem 11.9 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p 
|- P = ( Base ` G )
cgraid.i 
|- I = ( Itv ` G )
cgraid.g 
|- ( ph -> G e. TarskiG )
cgraid.k 
|- K = ( hlG ` G )
cgraid.a 
|- ( ph -> A e. P )
cgraid.b 
|- ( ph -> B e. P )
cgraid.c 
|- ( ph -> C e. P )
cgraid.1 
|- ( ph -> A =/= B )
cgraid.2 
|- ( ph -> B =/= C )
Assertion cgraswap 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" C B A "> )

Proof

Step Hyp Ref Expression
1 cgraid.p 
 |-  P = ( Base ` G )
2 cgraid.i 
 |-  I = ( Itv ` G )
3 cgraid.g 
 |-  ( ph -> G e. TarskiG )
4 cgraid.k 
 |-  K = ( hlG ` G )
5 cgraid.a 
 |-  ( ph -> A e. P )
6 cgraid.b 
 |-  ( ph -> B e. P )
7 cgraid.c 
 |-  ( ph -> C e. P )
8 cgraid.1 
 |-  ( ph -> A =/= B )
9 cgraid.2 
 |-  ( ph -> B =/= C )
10 eqid 
 |-  ( dist ` G ) = ( dist ` G )
11 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
12 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> G e. TarskiG )
13 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> A e. P )
14 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> B e. P )
15 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> C e. P )
16 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> x e. P )
17 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> y e. P )
18 simprlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) )
19 1 10 2 12 14 16 14 13 18 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x ( dist ` G ) B ) = ( A ( dist ` G ) B ) )
20 19 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( A ( dist ` G ) B ) = ( x ( dist ` G ) B ) )
21 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) )
22 21 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( B ( dist ` G ) C ) = ( B ( dist ` G ) y ) )
23 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
24 simprll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> x ( K ` B ) C )
25 1 2 4 16 15 14 12 23 24 hlln 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> x e. ( C ( LineG ` G ) B ) )
26 25 orcd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x e. ( C ( LineG ` G ) B ) \/ C = B ) )
27 1 23 2 12 15 14 16 26 colrot1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C e. ( B ( LineG ` G ) x ) \/ B = x ) )
28 eqid 
 |-  ( leG ` G ) = ( leG ` G )
29 1 2 4 16 15 14 12 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x ( K ` B ) C <-> ( x =/= B /\ C =/= B /\ ( x e. ( B I C ) \/ C e. ( B I x ) ) ) ) )
30 24 29 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x =/= B /\ C =/= B /\ ( x e. ( B I C ) \/ C e. ( B I x ) ) ) )
31 30 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x e. ( B I C ) \/ C e. ( B I x ) ) )
32 31 orcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C e. ( B I x ) \/ x e. ( B I C ) ) )
33 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> y ( K ` B ) A )
34 1 2 4 17 13 14 12 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( y ( K ` B ) A <-> ( y =/= B /\ A =/= B /\ ( y e. ( B I A ) \/ A e. ( B I y ) ) ) ) )
35 33 34 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( y =/= B /\ A =/= B /\ ( y e. ( B I A ) \/ A e. ( B I y ) ) ) )
36 35 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( y e. ( B I A ) \/ A e. ( B I y ) ) )
37 1 10 2 28 12 14 15 16 14 14 17 13 32 36 22 18 tgcgrsub2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C ( dist ` G ) x ) = ( y ( dist ` G ) A ) )
38 1 10 11 12 14 15 16 14 17 13 22 37 19 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> <" B C x "> ( cgrG ` G ) <" B y A "> )
39 1 10 2 12 15 17 axtgcgrrflx 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C ( dist ` G ) y ) = ( y ( dist ` G ) C ) )
40 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> B =/= C )
41 1 23 2 12 14 15 16 11 14 17 10 17 13 15 27 38 21 39 40 tgfscgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( x ( dist ` G ) y ) = ( A ( dist ` G ) C ) )
42 1 10 2 12 16 17 13 15 41 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( y ( dist ` G ) x ) = ( C ( dist ` G ) A ) )
43 42 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C ( dist ` G ) A ) = ( y ( dist ` G ) x ) )
44 1 10 11 12 13 14 15 16 14 17 20 22 43 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" x B y "> )
45 44 24 33 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) C /\ y ( K ` B ) A ) )
46 9 necomd 
 |-  ( ph -> C =/= B )
47 8 necomd 
 |-  ( ph -> B =/= A )
48 1 2 4 6 6 5 3 7 10 46 47 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) )
49 1 2 4 6 6 7 3 5 10 8 9 hlcgrex 
 |-  ( ph -> E. y e. P ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) )
50 reeanv 
 |-  ( E. x e. P E. y e. P ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) <-> ( E. x e. P ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ E. y e. P ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) )
51 48 49 50 sylanbrc 
 |-  ( ph -> E. x e. P E. y e. P ( ( x ( K ` B ) C /\ ( B ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` B ) A /\ ( B ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) )
52 45 51 reximddv2 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) C /\ y ( K ` B ) A ) )
53 1 2 4 3 5 6 7 7 6 5 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" C B A "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) C /\ y ( K ` B ) A ) ) )
54 52 53 mpbird 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" C B A "> )