Metamath Proof Explorer

Theorem trgcopyeu

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Hypotheses trgcopy.p 
|- P = ( Base ` G )
trgcopy.m 
|- .- = ( dist ` G )
trgcopy.i 
|- I = ( Itv ` G )
trgcopy.l 
|- L = ( LineG ` G )
trgcopy.k 
|- K = ( hlG ` G )
trgcopy.g 
|- ( ph -> G e. TarskiG )
trgcopy.a 
|- ( ph -> A e. P )
trgcopy.b 
|- ( ph -> B e. P )
trgcopy.c 
|- ( ph -> C e. P )
trgcopy.d 
|- ( ph -> D e. P )
trgcopy.e 
|- ( ph -> E e. P )
trgcopy.f 
|- ( ph -> F e. P )
trgcopy.1 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
trgcopy.2 
|- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
trgcopy.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
Assertion trgcopyeu 
|- ( ph -> E! f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )

Proof

Step Hyp Ref Expression
1 trgcopy.p 
 |-  P = ( Base ` G )
2 trgcopy.m 
 |-  .- = ( dist ` G )
3 trgcopy.i 
 |-  I = ( Itv ` G )
4 trgcopy.l 
 |-  L = ( LineG ` G )
5 trgcopy.k 
 |-  K = ( hlG ` G )
6 trgcopy.g 
 |-  ( ph -> G e. TarskiG )
7 trgcopy.a 
 |-  ( ph -> A e. P )
8 trgcopy.b 
 |-  ( ph -> B e. P )
9 trgcopy.c 
 |-  ( ph -> C e. P )
10 trgcopy.d 
 |-  ( ph -> D e. P )
11 trgcopy.e 
 |-  ( ph -> E e. P )
12 trgcopy.f 
 |-  ( ph -> F e. P )
13 trgcopy.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 trgcopy.2 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
15 trgcopy.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 trgcopy 
 |-  ( ph -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
17 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> G e. TarskiG )
18 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> A e. P )
19 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> B e. P )
20 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> C e. P )
21 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> D e. P )
22 11 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> E e. P )
23 12 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> F e. P )
24 13 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> -. ( A e. ( B L C ) \/ B = C ) )
25 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> -. ( D e. ( E L F ) \/ E = F ) )
26 15 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> ( A .- B ) = ( D .- E ) )
27 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
28 27 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( x e. ( P \ ( D L E ) ) <-> a e. ( P \ ( D L E ) ) ) )
29 simpr 
 |-  ( ( x = a /\ y = b ) -> y = b )
30 29 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( y e. ( P \ ( D L E ) ) <-> b e. ( P \ ( D L E ) ) ) )
31 28 30 anbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( x e. ( P \ ( D L E ) ) /\ y e. ( P \ ( D L E ) ) ) <-> ( a e. ( P \ ( D L E ) ) /\ b e. ( P \ ( D L E ) ) ) ) )
32 simpr 
 |-  ( ( ( x = a /\ y = b ) /\ z = t ) -> z = t )
33 simpll 
 |-  ( ( ( x = a /\ y = b ) /\ z = t ) -> x = a )
34 simplr 
 |-  ( ( ( x = a /\ y = b ) /\ z = t ) -> y = b )
35 33 34 oveq12d 
 |-  ( ( ( x = a /\ y = b ) /\ z = t ) -> ( x I y ) = ( a I b ) )
36 32 35 eleq12d 
 |-  ( ( ( x = a /\ y = b ) /\ z = t ) -> ( z e. ( x I y ) <-> t e. ( a I b ) ) )
37 36 cbvrexdva 
 |-  ( ( x = a /\ y = b ) -> ( E. z e. ( D L E ) z e. ( x I y ) <-> E. t e. ( D L E ) t e. ( a I b ) ) )
38 31 37 anbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( x e. ( P \ ( D L E ) ) /\ y e. ( P \ ( D L E ) ) ) /\ E. z e. ( D L E ) z e. ( x I y ) ) <-> ( ( a e. ( P \ ( D L E ) ) /\ b e. ( P \ ( D L E ) ) ) /\ E. t e. ( D L E ) t e. ( a I b ) ) ) )
39 38 cbvopabv 
 |-  { <. x , y >. | ( ( x e. ( P \ ( D L E ) ) /\ y e. ( P \ ( D L E ) ) ) /\ E. z e. ( D L E ) z e. ( x I y ) ) } = { <. a , b >. | ( ( a e. ( P \ ( D L E ) ) /\ b e. ( P \ ( D L E ) ) ) /\ E. t e. ( D L E ) t e. ( a I b ) ) }
40 simp-5r 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> f e. P )
41 simp-4r 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> k e. P )
42 simpllr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
43 42 simpld 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> <" A B C "> ( cgrG ` G ) <" D E f "> )
44 simplr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> <" A B C "> ( cgrG ` G ) <" D E k "> )
45 42 simprd 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> f ( ( hpG ` G ) ` ( D L E ) ) F )
46 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> k ( ( hpG ` G ) ` ( D L E ) ) F )
47 1 2 3 4 5 17 18 19 20 21 22 23 24 25 26 39 40 41 43 44 45 46 trgcopyeulem 
 |-  ( ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ <" A B C "> ( cgrG ` G ) <" D E k "> ) /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) -> f = k )
48 47 anasss 
 |-  ( ( ( ( ( ph /\ f e. P ) /\ k e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> f = k )
49 48 expl 
 |-  ( ( ( ph /\ f e. P ) /\ k e. P ) -> ( ( ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) /\ ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> f = k ) )
50 49 anasss 
 |-  ( ( ph /\ ( f e. P /\ k e. P ) ) -> ( ( ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) /\ ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> f = k ) )
51 50 ralrimivva 
 |-  ( ph -> A. f e. P A. k e. P ( ( ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) /\ ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> f = k ) )
52 eqidd 
 |-  ( f = k -> D = D )
53 eqidd 
 |-  ( f = k -> E = E )
54 id 
 |-  ( f = k -> f = k )
55 52 53 54 s3eqd 
 |-  ( f = k -> <" D E f "> = <" D E k "> )
56 55 breq2d 
 |-  ( f = k -> ( <" A B C "> ( cgrG ` G ) <" D E f "> <-> <" A B C "> ( cgrG ` G ) <" D E k "> ) )
57 breq1 
 |-  ( f = k -> ( f ( ( hpG ` G ) ` ( D L E ) ) F <-> k ( ( hpG ` G ) ` ( D L E ) ) F ) )
58 56 57 anbi12d 
 |-  ( f = k -> ( ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) <-> ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) )
59 58 reu4 
 |-  ( 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 "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) /\ A. f e. P A. k e. P ( ( ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) /\ ( <" A B C "> ( cgrG ` G ) <" D E k "> /\ k ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> f = k ) ) )
60 16 51 59 sylanbrc 
 |-  ( ph -> E! f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )