Metamath Proof Explorer


Theorem outsideofeu

Description: Given a nondegenerate ray, there is a unique point congruent to the segment B C lying on the ray A R . Theorem 6.11 of Schwabhauser p. 44. (Contributed by Scott Fenton, 23-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofeu NA𝔼NR𝔼NB𝔼NC𝔼NRABC∃!x𝔼NAOutsideOfxRAxCgrBC

Proof

Step Hyp Ref Expression
1 segcon2 NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRBtwnAxxBtwnARAxCgrBC
2 1 adantr NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼NRBtwnAxxBtwnARAxCgrBC
3 simpl1 NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NN
4 simpl2l NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NA𝔼N
5 simpr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Nx𝔼N
6 simpl2r NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NR𝔼N
7 broutsideof2 NA𝔼Nx𝔼NR𝔼NAOutsideOfxRxARAxBtwnARRBtwnAx
8 3 4 5 6 7 syl13anc NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NAOutsideOfxRxARAxBtwnARRBtwnAx
9 8 adantr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCAOutsideOfxRxARAxBtwnARRBtwnAx
10 simp3 xARAxBtwnARRBtwnAxxBtwnARRBtwnAx
11 simpllr RABCAxCgrBCxBtwnARRBtwnAxBC
12 11 adantl NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxBC
13 simprlr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxAxCgrBC
14 simp2l NA𝔼NR𝔼NB𝔼NC𝔼NA𝔼N
15 14 anim1i NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NA𝔼Nx𝔼N
16 simpl3 NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NB𝔼NC𝔼N
17 cgrdegen NA𝔼Nx𝔼NB𝔼NC𝔼NAxCgrBCA=xB=C
18 3 15 16 17 syl3anc NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NAxCgrBCA=xB=C
19 18 adantr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxAxCgrBCA=xB=C
20 13 19 mpd NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxA=xB=C
21 20 necon3bid NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxAxBC
22 12 21 mpbird NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxAx
23 22 necomd NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxxA
24 simplll RABCAxCgrBCxBtwnARRBtwnAxRA
25 24 adantl NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxRA
26 simprr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxxBtwnARRBtwnAx
27 23 25 26 3jca NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxxARAxBtwnARRBtwnAx
28 27 expr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxBtwnARRBtwnAxxARAxBtwnARRBtwnAx
29 10 28 impbid2 NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCxARAxBtwnARRBtwnAxxBtwnARRBtwnAx
30 9 29 bitrd NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCAOutsideOfxRxBtwnARRBtwnAx
31 orcom xBtwnARRBtwnAxRBtwnAxxBtwnAR
32 30 31 bitrdi NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCAOutsideOfxRRBtwnAxxBtwnAR
33 32 expr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAxCgrBCAOutsideOfxRRBtwnAxxBtwnAR
34 33 pm5.32rd NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼NRABCAOutsideOfxRAxCgrBCRBtwnAxxBtwnARAxCgrBC
35 34 an32s NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼NAOutsideOfxRAxCgrBCRBtwnAxxBtwnARAxCgrBC
36 35 rexbidva NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼NAOutsideOfxRAxCgrBCx𝔼NRBtwnAxxBtwnARAxCgrBC
37 2 36 mpbird NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼NAOutsideOfxRAxCgrBC
38 simpl1 NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NN
39 simpl2l NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NA𝔼N
40 simpl2r NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NR𝔼N
41 simpl3l NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NB𝔼N
42 39 40 41 3jca NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NA𝔼NR𝔼NB𝔼N
43 simpl3r NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NC𝔼N
44 simprl NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼Nx𝔼N
45 simprr NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼Ny𝔼N
46 43 44 45 3jca NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NC𝔼Nx𝔼Ny𝔼N
47 38 42 46 3jca NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NNA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼N
48 simpr RABCAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBC
49 outsideofeq NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
50 49 imp NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
51 47 48 50 syl2an NA𝔼NR𝔼NB𝔼NC𝔼Nx𝔼Ny𝔼NRABCAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
52 51 an4s NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
53 52 exp32 NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
54 53 ralrimivv NA𝔼NR𝔼NB𝔼NC𝔼NRABCx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
55 opeq1 x=yxR=yR
56 55 breq2d x=yAOutsideOfxRAOutsideOfyR
57 opeq2 x=yAx=Ay
58 57 breq1d x=yAxCgrBCAyCgrBC
59 56 58 anbi12d x=yAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBC
60 59 reu4 ∃!x𝔼NAOutsideOfxRAxCgrBCx𝔼NAOutsideOfxRAxCgrBCx𝔼Ny𝔼NAOutsideOfxRAxCgrBCAOutsideOfyRAyCgrBCx=y
61 37 54 60 sylanbrc NA𝔼NR𝔼NB𝔼NC𝔼NRABC∃!x𝔼NAOutsideOfxRAxCgrBC
62 61 ex NA𝔼NR𝔼NB𝔼NC𝔼NRABC∃!x𝔼NAOutsideOfxRAxCgrBC