Metamath Proof Explorer

Theorem cgrahl

Description: Angle congruence preserves null 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 "> )
cgrahl.k 
|- K = ( hlG ` G )
cgrahl.2 
|- ( ph -> A ( K ` B ) C )
Assertion cgrahl 
|- ( ph -> D ( K ` E ) 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 cgrahl.k 
 |-  K = ( hlG ` G )
13 cgrahl.2 
 |-  ( ph -> A ( K ` B ) C )
14 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D e. P )
15 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y e. P )
16 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> F e. P )
17 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> G e. TarskiG )
18 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E e. P )
19 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x e. P )
20 simpr2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x ( K ` E ) D )
21 1 2 12 19 14 18 17 20 hlcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D ( K ` E ) x )
22 1 2 12 19 14 18 17 20 hlne1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x =/= E )
23 simpr3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y ( K ` E ) F )
24 1 2 12 15 16 18 17 23 hlne1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y =/= E )
25 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
26 17 adantr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> G e. TarskiG )
27 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> B e. P )
28 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> A e. P )
29 7 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> C e. P )
30 18 adantr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> E e. P )
31 19 adantr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> x e. P )
32 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> y e. P )
33 simplr1 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
34 1 3 2 25 26 28 27 29 31 30 32 33 cgr3swap12 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> <" B A C "> ( cgrG ` G ) <" E x y "> )
35 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> A e. ( B I C ) )
36 1 3 2 25 26 27 28 29 30 31 32 34 35 tgbtwnxfr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> x e. ( E I y ) )
37 36 orcd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ A e. ( B I C ) ) -> ( x e. ( E I y ) \/ y e. ( E I x ) ) )
38 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> G e. TarskiG )
39 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> B e. P )
40 7 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> C e. P )
41 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> A e. P )
42 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> E e. P )
43 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> y e. P )
44 19 adantr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> x e. P )
45 simplr1 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
46 1 3 2 25 38 41 39 40 44 42 43 45 cgr3rotl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> <" B C A "> ( cgrG ` G ) <" E y x "> )
47 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> C e. ( B I A ) )
48 1 3 2 25 38 39 40 41 42 43 44 46 47 tgbtwnxfr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> y e. ( E I x ) )
49 48 olcd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) /\ C e. ( B I A ) ) -> ( x e. ( E I y ) \/ y e. ( E I x ) ) )
50 1 2 12 5 7 6 4 ishlg 
 |-  ( ph -> ( A ( K ` B ) C <-> ( A =/= B /\ C =/= B /\ ( A e. ( B I C ) \/ C e. ( B I A ) ) ) ) )
51 13 50 mpbid 
 |-  ( ph -> ( A =/= B /\ C =/= B /\ ( A e. ( B I C ) \/ C e. ( B I A ) ) ) )
52 51 simp3d 
 |-  ( ph -> ( A e. ( B I C ) \/ C e. ( B I A ) ) )
53 52 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A e. ( B I C ) \/ C e. ( B I A ) ) )
54 37 49 53 mpjaodan 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x e. ( E I y ) \/ y e. ( E I x ) ) )
55 1 2 12 19 15 18 17 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x ( K ` E ) y <-> ( x =/= E /\ y =/= E /\ ( x e. ( E I y ) \/ y e. ( E I x ) ) ) ) )
56 22 24 54 55 mpbir3and 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x ( K ` E ) y )
57 1 2 12 14 19 15 17 18 21 56 hltr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D ( K ` E ) y )
58 1 2 12 14 15 16 17 18 57 23 hltr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D ( K ` E ) F )
59 1 2 12 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 ( K ` E ) D /\ y ( K ` E ) F ) ) )
60 11 59 mpbid 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) )
61 58 60 r19.29vva 
 |-  ( ph -> D ( K ` E ) F )