Metamath Proof Explorer

Theorem sacgr

Description: Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020) (Proof shortened by Igor Ieskov, 16-Feb-2023)

Ref Expression
Hypotheses dfcgra2.p 
|- P = ( Base ` G )
dfcgra2.i 
|- I = ( Itv ` G )
dfcgra2.m 
|- .- = ( dist ` G )
dfcgra2.g 
|- ( ph -> G e. TarskiG )
dfcgra2.a 
|- ( ph -> A e. P )
dfcgra2.b 
|- ( ph -> B e. P )
dfcgra2.c 
|- ( ph -> C e. P )
dfcgra2.d 
|- ( ph -> D e. P )
dfcgra2.e 
|- ( ph -> E e. P )
dfcgra2.f 
|- ( ph -> F e. P )
sacgr.x 
|- ( ph -> X e. P )
sacgr.y 
|- ( ph -> Y e. P )
sacgr.1 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
sacgr.2 
|- ( ph -> B e. ( A I X ) )
sacgr.3 
|- ( ph -> E e. ( D I Y ) )
sacgr.4 
|- ( ph -> B =/= X )
sacgr.5 
|- ( ph -> E =/= Y )
Assertion sacgr 
|- ( ph -> <" X B C "> ( cgrA ` G ) <" Y E F "> )

Proof

Step Hyp Ref Expression
1 dfcgra2.p 
 |-  P = ( Base ` G )
2 dfcgra2.i 
 |-  I = ( Itv ` G )
3 dfcgra2.m 
 |-  .- = ( dist ` G )
4 dfcgra2.g 
 |-  ( ph -> G e. TarskiG )
5 dfcgra2.a 
 |-  ( ph -> A e. P )
6 dfcgra2.b 
 |-  ( ph -> B e. P )
7 dfcgra2.c 
 |-  ( ph -> C e. P )
8 dfcgra2.d 
 |-  ( ph -> D e. P )
9 dfcgra2.e 
 |-  ( ph -> E e. P )
10 dfcgra2.f 
 |-  ( ph -> F e. P )
11 sacgr.x 
 |-  ( ph -> X e. P )
12 sacgr.y 
 |-  ( ph -> Y e. P )
13 sacgr.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
14 sacgr.2 
 |-  ( ph -> B e. ( A I X ) )
15 sacgr.3 
 |-  ( ph -> E e. ( D I Y ) )
16 sacgr.4 
 |-  ( ph -> B =/= X )
17 sacgr.5 
 |-  ( ph -> E =/= Y )
18 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
19 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> G e. TarskiG )
20 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> X e. P )
21 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> B e. P )
22 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> C e. P )
23 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> Y e. P )
24 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. P )
25 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> F e. P )
26 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
27 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
28 eqid 
 |-  ( ( pInvG ` G ) ` E ) = ( ( pInvG ` G ) ` E )
29 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> x e. P )
30 1 3 2 26 27 19 24 28 29 mircl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` E ) ` x ) e. P )
31 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> y e. P )
32 eqid 
 |-  ( ( pInvG ` G ) ` B ) = ( ( pInvG ` G ) ` B )
33 1 3 2 26 27 4 6 32 11 mirmir 
 |-  ( ph -> ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) = X )
34 eqidd 
 |-  ( ph -> B = B )
35 eqidd 
 |-  ( ph -> C = C )
36 33 34 35 s3eqd 
 |-  ( ph -> <" ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) B C "> = <" X B C "> )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) B C "> = <" X B C "> )
38 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
39 1 3 2 26 27 4 6 32 11 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` B ) ` X ) e. P )
40 39 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` B ) ` X ) e. P )
41 16 necomd 
 |-  ( ph -> X =/= B )
42 1 3 2 26 27 4 6 32 11 41 mirne 
 |-  ( ph -> ( ( ( pInvG ` G ) ` B ) ` X ) =/= B )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` B ) ` X ) =/= B )
44 simpr1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> )
45 1 3 2 26 27 19 38 32 28 40 21 29 24 22 31 43 44 mirtrcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) B C "> ( cgrG ` G ) <" ( ( ( pInvG ` G ) ` E ) ` x ) E y "> )
46 37 45 eqbrtrrd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" X B C "> ( cgrG ` G ) <" ( ( ( pInvG ` G ) ` E ) ` x ) E y "> )
47 17 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E =/= Y )
48 47 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> Y =/= E )
49 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> D e. P )
50 simpr2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> x ( ( hlG ` G ) ` E ) D )
51 1 2 18 29 49 24 19 50 hlne1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> x =/= E )
52 1 3 2 26 27 19 24 28 29 51 mirne 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` E ) ` x ) =/= E )
53 1 2 18 29 49 24 19 50 hlcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> D ( ( hlG ` G ) ` E ) x )
54 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( D I Y ) )
55 1 2 18 49 29 23 19 24 53 54 btwnhl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( x I Y ) )
56 1 3 2 19 29 24 23 55 tgbtwncom 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( Y I x ) )
57 1 3 2 26 27 19 24 28 29 mirmir 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` E ) ` ( ( ( pInvG ` G ) ` E ) ` x ) ) = x )
58 57 oveq2d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( Y I ( ( ( pInvG ` G ) ` E ) ` ( ( ( pInvG ` G ) ` E ) ` x ) ) ) = ( Y I x ) )
59 56 58 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( Y I ( ( ( pInvG ` G ) ` E ) ` ( ( ( pInvG ` G ) ` E ) ` x ) ) ) )
60 1 3 2 26 27 19 28 18 24 23 30 24 48 52 59 mirhl2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> Y ( ( hlG ` G ) ` E ) ( ( ( pInvG ` G ) ` E ) ` x ) )
61 1 2 18 23 30 24 19 60 hlcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> ( ( ( pInvG ` G ) ` E ) ` x ) ( ( hlG ` G ) ` E ) Y )
62 simpr3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> y ( ( hlG ` G ) ` E ) F )
63 1 2 18 19 20 21 22 23 24 25 30 31 46 61 62 iscgrad 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" X B C "> ( cgrA ` G ) <" Y E F "> )
64 1 2 18 4 5 6 7 8 9 10 13 cgrane2 
 |-  ( ph -> B =/= C )
65 1 2 4 18 39 6 7 42 64 cgraid 
 |-  ( ph -> <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrA ` G ) <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> )
66 1 2 18 4 5 6 7 8 9 10 13 cgrane1 
 |-  ( ph -> A =/= B )
67 33 oveq2d 
 |-  ( ph -> ( A I ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) ) = ( A I X ) )
68 14 67 eleqtrrd 
 |-  ( ph -> B e. ( A I ( ( ( pInvG ` G ) ` B ) ` ( ( ( pInvG ` G ) ` B ) ` X ) ) ) )
69 1 3 2 26 27 4 32 18 6 5 39 5 66 42 68 mirhl2 
 |-  ( ph -> A ( ( hlG ` G ) ` B ) ( ( ( pInvG ` G ) ` B ) ` X ) )
70 1 2 18 4 39 6 7 39 6 7 65 5 69 cgrahl1 
 |-  ( ph -> <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrA ` G ) <" A B C "> )
71 1 2 4 18 39 6 7 5 6 7 70 8 9 10 13 cgratr 
 |-  ( ph -> <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrA ` G ) <" D E F "> )
72 1 2 18 4 39 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) )
73 71 72 mpbid 
 |-  ( ph -> E. x e. P E. y e. P ( <" ( ( ( pInvG ` G ) ` B ) ` X ) B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) )
74 63 73 r19.29vva 
 |-  ( ph -> <" X B C "> ( cgrA ` G ) <" Y E F "> )