Metamath Proof Explorer

Theorem cgracom

Description: Angle congruence commutes. Theorem 11.7 of Schwabhauser p. 97. (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 )
cgracom.d 
|- ( ph -> D e. P )
cgracom.e 
|- ( ph -> E e. P )
cgracom.f 
|- ( ph -> F e. P )
cgracom.1 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
Assertion cgracom 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" A B C "> )

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 cgracom.d 
 |-  ( ph -> D e. P )
9 cgracom.e 
 |-  ( ph -> E e. P )
10 cgracom.f 
 |-  ( ph -> F e. P )
11 cgracom.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 eqid 
 |-  ( dist ` G ) = ( dist ` G )
13 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
14 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> G e. TarskiG )
15 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> D e. P )
16 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> E e. P )
17 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> F e. P )
18 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> x e. P )
19 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> B e. P )
20 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> y e. P )
21 simprlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) )
22 21 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( E ( dist ` G ) D ) = ( B ( dist ` G ) x ) )
23 1 12 2 14 16 15 19 18 22 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( D ( dist ` G ) E ) = ( x ( dist ` G ) B ) )
24 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) )
25 24 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( E ( dist ` G ) F ) = ( B ( dist ` G ) y ) )
26 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> A e. P )
27 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> C e. P )
28 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
29 simprll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> x ( K ` B ) A )
30 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> y ( K ` B ) C )
31 1 2 4 14 26 19 27 15 16 17 28 18 12 20 29 30 21 24 cgracgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( x ( dist ` G ) y ) = ( D ( dist ` G ) F ) )
32 31 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( D ( dist ` G ) F ) = ( x ( dist ` G ) y ) )
33 1 12 2 14 15 17 18 20 32 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( F ( dist ` G ) D ) = ( y ( dist ` G ) x ) )
34 1 12 13 14 15 16 17 18 19 20 23 25 33 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> <" D E F "> ( cgrG ` G ) <" x B y "> )
35 34 29 30 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) ) -> ( <" D E F "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) A /\ y ( K ` B ) C ) )
36 1 2 4 3 5 6 7 8 9 10 11 cgrane1 
 |-  ( ph -> A =/= B )
37 1 2 4 3 5 6 7 8 9 10 11 cgrane3 
 |-  ( ph -> E =/= D )
38 1 2 4 6 9 8 3 5 12 36 37 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) )
39 1 2 4 3 5 6 7 8 9 10 11 cgrane2 
 |-  ( ph -> B =/= C )
40 39 necomd 
 |-  ( ph -> C =/= B )
41 1 2 4 3 5 6 7 8 9 10 11 cgrane4 
 |-  ( ph -> E =/= F )
42 1 2 4 6 9 10 3 7 12 40 41 hlcgrex 
 |-  ( ph -> E. y e. P ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) )
43 reeanv 
 |-  ( E. x e. P E. y e. P ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) <-> ( E. x e. P ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ E. y e. P ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) )
44 38 42 43 sylanbrc 
 |-  ( ph -> E. x e. P E. y e. P ( ( x ( K ` B ) A /\ ( B ( dist ` G ) x ) = ( E ( dist ` G ) D ) ) /\ ( y ( K ` B ) C /\ ( B ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) )
45 35 44 reximddv2 
 |-  ( ph -> E. x e. P E. y e. P ( <" D E F "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) A /\ y ( K ` B ) C ) )
46 1 2 4 3 8 9 10 5 6 7 iscgra 
 |-  ( ph -> ( <" D E F "> ( cgrA ` G ) <" A B C "> <-> E. x e. P E. y e. P ( <" D E F "> ( cgrG ` G ) <" x B y "> /\ x ( K ` B ) A /\ y ( K ` B ) C ) ) )
47 45 46 mpbird 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" A B C "> )