Metamath Proof Explorer

Theorem cgrabtwn

Description: Angle congruence preserves flat angles. Part of Theorem 11.21 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses cgracol.p 
|- P = ( Base ` G )
cgracol.i 
|- I = ( Itv ` G )
cgracol.m 
|- .- = ( dist ` G )
cgracol.g 
|- ( ph -> G e. TarskiG )
cgracol.a 
|- ( ph -> A e. P )
cgracol.b 
|- ( ph -> B e. P )
cgracol.c 
|- ( ph -> C e. P )
cgracol.d 
|- ( ph -> D e. P )
cgracol.e 
|- ( ph -> E e. P )
cgracol.f 
|- ( ph -> F e. P )
cgracol.1 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
cgrabtwn.2 
|- ( ph -> B e. ( A I C ) )
Assertion cgrabtwn 
|- ( ph -> E e. ( D I F ) )

Proof

Step Hyp Ref Expression
1 cgracol.p 
 |-  P = ( Base ` G )
2 cgracol.i 
 |-  I = ( Itv ` G )
3 cgracol.m 
 |-  .- = ( dist ` G )
4 cgracol.g 
 |-  ( ph -> G e. TarskiG )
5 cgracol.a 
 |-  ( ph -> A e. P )
6 cgracol.b 
 |-  ( ph -> B e. P )
7 cgracol.c 
 |-  ( ph -> C e. P )
8 cgracol.d 
 |-  ( ph -> D e. P )
9 cgracol.e 
 |-  ( ph -> E e. P )
10 cgracol.f 
 |-  ( ph -> F e. P )
11 cgracol.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 cgrabtwn.2 
 |-  ( ph -> B e. ( A I C ) )
13 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
14 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> x e. P )
15 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> D e. P )
16 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> F e. P )
17 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> G e. TarskiG )
18 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. P )
19 simpr2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> x ( ( hlG ` G ) ` E ) D )
20 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> y e. P )
21 simpr3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> y ( ( hlG ` G ) ` E ) F )
22 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
23 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> A e. P )
24 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> B e. P )
25 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> C e. P )
26 simpr1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
27 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> B e. ( A I C ) )
28 1 3 2 22 17 23 24 25 14 18 20 26 27 tgbtwnxfr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( x I y ) )
29 1 3 2 17 14 18 20 28 tgbtwncom 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( y I x ) )
30 1 2 13 20 16 14 17 18 21 29 btwnhl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( F I x ) )
31 1 3 2 17 16 18 14 30 tgbtwncom 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( x I F ) )
32 1 2 13 14 15 16 17 18 19 31 btwnhl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) -> E e. ( D I F ) )
33 1 2 13 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) )
34 11 33 mpbid 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) )
35 32 34 r19.29vva 
 |-  ( ph -> E e. ( D I F ) )