Metamath Proof Explorer

Theorem acopy

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. (Contributed by Thierry Arnoux, 9-Aug-2020)

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 )
acopy.l 
|- L = ( LineG ` G )
acopy.1 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
acopy.2 
|- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
Assertion acopy 
|- ( ph -> E. f e. P ( <" A B C "> ( cgrA ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L 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 acopy.l 
 |-  L = ( LineG ` G )
12 acopy.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13 acopy.2 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
14 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
15 4 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> G e. TarskiG )
16 5 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> A e. P )
17 6 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> B e. P )
18 7 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> C e. P )
19 simplr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d e. P )
20 9 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E e. P )
21 10 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> F e. P )
22 12 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( A e. ( B L C ) \/ B = C ) )
23 8 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> D e. P )
24 13 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( D e. ( E L F ) \/ E = F ) )
25 simprl 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d ( ( hlG ` G ) ` E ) D )
26 1 2 14 19 23 20 15 11 25 hlln 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d e. ( D L E ) )
27 1 2 14 19 23 20 15 25 hlne1 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d =/= E )
28 1 2 11 15 23 20 21 19 24 26 27 ncolncol 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( d e. ( E L F ) \/ E = F ) )
29 simprr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( E .- d ) = ( B .- A ) )
30 29 eqcomd 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( B .- A ) = ( E .- d ) )
31 1 3 2 15 17 16 20 19 30 tgcgrcomlr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( A .- B ) = ( d .- E ) )
32 1 3 2 11 14 15 16 17 18 19 20 21 22 28 31 trgcopy 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" d E f "> /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) )
33 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> G e. TarskiG )
34 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> A e. P )
35 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> B e. P )
36 18 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> C e. P )
37 19 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> d e. P )
38 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> E e. P )
39 simplr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> f e. P )
40 1 2 11 4 5 6 7 12 ncolne1 
 |-  ( ph -> A =/= B )
41 40 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> A =/= B )
42 1 11 2 4 6 7 5 12 ncolrot1 
 |-  ( ph -> -. ( B e. ( C L A ) \/ C = A ) )
43 1 2 11 4 6 7 5 42 ncolne1 
 |-  ( ph -> B =/= C )
44 43 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> B =/= C )
45 simpr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> <" A B C "> ( cgrG ` G ) <" d E f "> )
46 1 2 33 14 34 35 36 37 38 39 41 44 45 cgrcgra 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> <" A B C "> ( cgrA ` G ) <" d E f "> )
47 23 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> D e. P )
48 25 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> d ( ( hlG ` G ) ` E ) D )
49 1 2 14 37 47 38 33 48 hlcomd 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> D ( ( hlG ` G ) ` E ) d )
50 1 2 14 33 34 35 36 37 38 39 46 47 49 cgrahl1 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ <" A B C "> ( cgrG ` G ) <" d E f "> ) -> <" A B C "> ( cgrA ` G ) <" D E f "> )
51 50 ex 
 |-  ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) -> ( <" A B C "> ( cgrG ` G ) <" d E f "> -> <" A B C "> ( cgrA ` G ) <" D E f "> ) )
52 simpr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> f ( ( hpG ` G ) ` ( d L E ) ) F )
53 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> G e. TarskiG )
54 19 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> d e. P )
55 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> E e. P )
56 27 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> d =/= E )
57 1 2 11 4 8 9 10 13 ncolne1 
 |-  ( ph -> D =/= E )
58 1 2 11 4 8 9 57 tgelrnln 
 |-  ( ph -> ( D L E ) e. ran L )
59 58 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> ( D L E ) e. ran L )
60 26 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> d e. ( D L E ) )
61 1 2 11 4 8 9 57 tglinerflx2 
 |-  ( ph -> E e. ( D L E ) )
62 61 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> E e. ( D L E ) )
63 1 2 11 53 54 55 56 56 59 60 62 tglinethru 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> ( D L E ) = ( d L E ) )
64 63 fveq2d 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> ( ( hpG ` G ) ` ( D L E ) ) = ( ( hpG ` G ) ` ( d L E ) ) )
65 64 breqd 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> ( f ( ( hpG ` G ) ` ( D L E ) ) F <-> f ( ( hpG ` G ) ` ( d L E ) ) F ) )
66 52 65 mpbird 
 |-  ( ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> f ( ( hpG ` G ) ` ( D L E ) ) F )
67 66 ex 
 |-  ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) -> ( f ( ( hpG ` G ) ` ( d L E ) ) F -> f ( ( hpG ` G ) ` ( D L E ) ) F ) )
68 51 67 anim12d 
 |-  ( ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) /\ f e. P ) -> ( ( <" A B C "> ( cgrG ` G ) <" d E f "> /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> ( <" A B C "> ( cgrA ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) )
69 68 reximdva 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( E. f e. P ( <" A B C "> ( cgrG ` G ) <" d E f "> /\ f ( ( hpG ` G ) ` ( d L E ) ) F ) -> E. f e. P ( <" A B C "> ( cgrA ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) )
70 32 69 mpd 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E. f e. P ( <" A B C "> ( cgrA ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
71 40 necomd 
 |-  ( ph -> B =/= A )
72 1 2 14 9 6 5 4 8 3 57 71 hlcgrex 
 |-  ( ph -> E. d e. P ( d ( ( hlG ` G ) ` E ) D /\ ( E .- d ) = ( B .- A ) ) )
73 70 72 r19.29a 
 |-  ( ph -> E. f e. P ( <" A B C "> ( cgrA ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )