Metamath Proof Explorer

Theorem footexlem1

Description: Lemma for footex . (Contributed by Thierry Arnoux, 19-Oct-2019) (Revised by Thierry Arnoux, 1-Jul-2023)

Ref Expression
Hypotheses isperp.p 
|- P = ( Base ` G )
isperp.d 
|- .- = ( dist ` G )
isperp.i 
|- I = ( Itv ` G )
isperp.l 
|- L = ( LineG ` G )
isperp.g 
|- ( ph -> G e. TarskiG )
isperp.a 
|- ( ph -> A e. ran L )
foot.x 
|- ( ph -> C e. P )
foot.y 
|- ( ph -> -. C e. A )
footexlem.e 
|- ( ph -> E e. P )
footexlem.f 
|- ( ph -> F e. P )
footexlem.r 
|- ( ph -> R e. P )
footexlem.x 
|- ( ph -> X e. P )
footexlem.y 
|- ( ph -> Y e. P )
footexlem.z 
|- ( ph -> Z e. P )
footexlem.d 
|- ( ph -> D e. P )
footexlem.1 
|- ( ph -> A = ( E L F ) )
footexlem.2 
|- ( ph -> E =/= F )
footexlem.3 
|- ( ph -> E e. ( F I Y ) )
footexlem.4 
|- ( ph -> ( E .- Y ) = ( E .- C ) )
footexlem.5 
|- ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) )
footexlem.6 
|- ( ph -> Y e. ( E I Z ) )
footexlem.7 
|- ( ph -> ( Y .- Z ) = ( Y .- R ) )
footexlem.q 
|- ( ph -> Q e. P )
footexlem.8 
|- ( ph -> Y e. ( R I Q ) )
footexlem.9 
|- ( ph -> ( Y .- Q ) = ( Y .- E ) )
footexlem.10 
|- ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
footexlem.11 
|- ( ph -> ( Y .- D ) = ( Y .- C ) )
footexlem.12 
|- ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) )
Assertion footexlem1 
|- ( ph -> X e. A )

Proof

Step Hyp Ref Expression
1 isperp.p 
 |-  P = ( Base ` G )
2 isperp.d 
 |-  .- = ( dist ` G )
3 isperp.i 
 |-  I = ( Itv ` G )
4 isperp.l 
 |-  L = ( LineG ` G )
5 isperp.g 
 |-  ( ph -> G e. TarskiG )
6 isperp.a 
 |-  ( ph -> A e. ran L )
7 foot.x 
 |-  ( ph -> C e. P )
8 foot.y 
 |-  ( ph -> -. C e. A )
9 footexlem.e 
 |-  ( ph -> E e. P )
10 footexlem.f 
 |-  ( ph -> F e. P )
11 footexlem.r 
 |-  ( ph -> R e. P )
12 footexlem.x 
 |-  ( ph -> X e. P )
13 footexlem.y 
 |-  ( ph -> Y e. P )
14 footexlem.z 
 |-  ( ph -> Z e. P )
15 footexlem.d 
 |-  ( ph -> D e. P )
16 footexlem.1 
 |-  ( ph -> A = ( E L F ) )
17 footexlem.2 
 |-  ( ph -> E =/= F )
18 footexlem.3 
 |-  ( ph -> E e. ( F I Y ) )
19 footexlem.4 
 |-  ( ph -> ( E .- Y ) = ( E .- C ) )
20 footexlem.5 
 |-  ( ph -> C = ( ( ( pInvG ` G ) ` R ) ` Y ) )
21 footexlem.6 
 |-  ( ph -> Y e. ( E I Z ) )
22 footexlem.7 
 |-  ( ph -> ( Y .- Z ) = ( Y .- R ) )
23 footexlem.q 
 |-  ( ph -> Q e. P )
24 footexlem.8 
 |-  ( ph -> Y e. ( R I Q ) )
25 footexlem.9 
 |-  ( ph -> ( Y .- Q ) = ( Y .- E ) )
26 footexlem.10 
 |-  ( ph -> Y e. ( ( ( ( pInvG ` G ) ` Z ) ` Q ) I D ) )
27 footexlem.11 
 |-  ( ph -> ( Y .- D ) = ( Y .- C ) )
28 footexlem.12 
 |-  ( ph -> D = ( ( ( pInvG ` G ) ` X ) ` C ) )
29 22 eqcomd 
 |-  ( ph -> ( Y .- R ) = ( Y .- Z ) )
30 17 necomd 
 |-  ( ph -> F =/= E )
31 1 3 4 5 10 9 13 30 18 btwnlng3 
 |-  ( ph -> Y e. ( F L E ) )
32 1 3 4 5 9 10 13 17 31 lncom 
 |-  ( ph -> Y e. ( E L F ) )
33 32 16 eleqtrrd 
 |-  ( ph -> Y e. A )
34 nelne2 
 |-  ( ( Y e. A /\ -. C e. A ) -> Y =/= C )
35 33 8 34 syl2anc 
 |-  ( ph -> Y =/= C )
36 35 necomd 
 |-  ( ph -> C =/= Y )
37 20 36 eqnetrrd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` R ) ` Y ) =/= Y )
38 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
39 eqid 
 |-  ( ( pInvG ` G ) ` R ) = ( ( pInvG ` G ) ` R )
40 1 2 3 4 38 5 11 39 13 mirinv 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` R ) ` Y ) = Y <-> R = Y ) )
41 40 necon3bid 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` R ) ` Y ) =/= Y <-> R =/= Y ) )
42 37 41 mpbid 
 |-  ( ph -> R =/= Y )
43 42 necomd 
 |-  ( ph -> Y =/= R )
44 1 2 3 5 13 11 13 14 29 43 tgcgrneq 
 |-  ( ph -> Y =/= Z )
45 44 necomd 
 |-  ( ph -> Z =/= Y )
46 eqid 
 |-  ( ( pInvG ` G ) ` Z ) = ( ( pInvG ` G ) ` Z )
47 eqid 
 |-  ( ( pInvG ` G ) ` X ) = ( ( pInvG ` G ) ` X )
48 1 2 3 4 38 5 14 46 23 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` Z ) ` Q ) e. P )
49 1 2 3 4 38 5 11 39 13 mirbtwn 
 |-  ( ph -> R e. ( ( ( ( pInvG ` G ) ` R ) ` Y ) I Y ) )
50 20 oveq1d 
 |-  ( ph -> ( C I Y ) = ( ( ( ( pInvG ` G ) ` R ) ` Y ) I Y ) )
51 49 50 eleqtrrd 
 |-  ( ph -> R e. ( C I Y ) )
52 1 2 3 5 7 11 13 23 42 51 24 tgbtwnouttr2 
 |-  ( ph -> Y e. ( C I Q ) )
53 1 2 3 5 7 13 23 52 tgbtwncom 
 |-  ( ph -> Y e. ( Q I C ) )
54 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
55 20 oveq2d 
 |-  ( ph -> ( E .- C ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) )
56 19 55 eqtrd 
 |-  ( ph -> ( E .- Y ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) )
57 1 2 3 4 38 5 9 11 13 israg 
 |-  ( ph -> ( <" E R Y "> e. ( raG ` G ) <-> ( E .- Y ) = ( E .- ( ( ( pInvG ` G ) ` R ) ` Y ) ) ) )
58 56 57 mpbird 
 |-  ( ph -> <" E R Y "> e. ( raG ` G ) )
59 1 2 3 5 9 13 9 7 19 tgcgrcomlr 
 |-  ( ph -> ( Y .- E ) = ( C .- E ) )
60 25 59 eqtr2d 
 |-  ( ph -> ( C .- E ) = ( Y .- Q ) )
61 1 3 4 5 9 10 17 tglinerflx1 
 |-  ( ph -> E e. ( E L F ) )
62 61 16 eleqtrrd 
 |-  ( ph -> E e. A )
63 nelne2 
 |-  ( ( E e. A /\ -. C e. A ) -> E =/= C )
64 62 8 63 syl2anc 
 |-  ( ph -> E =/= C )
65 64 necomd 
 |-  ( ph -> C =/= E )
66 1 2 3 5 7 9 13 23 60 65 tgcgrneq 
 |-  ( ph -> Y =/= Q )
67 66 necomd 
 |-  ( ph -> Q =/= Y )
68 1 2 3 5 11 13 23 24 tgbtwncom 
 |-  ( ph -> Y e. ( Q I R ) )
69 1 2 3 5 13 23 13 9 25 tgcgrcomlr 
 |-  ( ph -> ( Q .- Y ) = ( E .- Y ) )
70 1 2 3 5 23 9 axtgcgrrflx 
 |-  ( ph -> ( Q .- E ) = ( E .- Q ) )
71 25 eqcomd 
 |-  ( ph -> ( Y .- E ) = ( Y .- Q ) )
72 1 2 3 5 23 13 11 9 13 14 9 23 67 68 21 69 29 70 71 axtg5seg 
 |-  ( ph -> ( R .- E ) = ( Z .- Q ) )
73 1 2 3 5 11 9 14 23 72 tgcgrcomlr 
 |-  ( ph -> ( E .- R ) = ( Q .- Z ) )
74 1 2 3 5 13 11 13 14 29 tgcgrcomlr 
 |-  ( ph -> ( R .- Y ) = ( Z .- Y ) )
75 1 2 54 5 9 11 13 23 14 13 73 74 71 trgcgr 
 |-  ( ph -> <" E R Y "> ( cgrG ` G ) <" Q Z Y "> )
76 1 2 3 4 38 5 9 11 13 54 23 14 13 58 75 ragcgr 
 |-  ( ph -> <" Q Z Y "> e. ( raG ` G ) )
77 1 2 3 4 38 5 23 14 13 76 ragcom 
 |-  ( ph -> <" Y Z Q "> e. ( raG ` G ) )
78 1 2 3 4 38 5 13 14 23 israg 
 |-  ( ph -> ( <" Y Z Q "> e. ( raG ` G ) <-> ( Y .- Q ) = ( Y .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) ) )
79 77 78 mpbid 
 |-  ( ph -> ( Y .- Q ) = ( Y .- ( ( ( pInvG ` G ) ` Z ) ` Q ) ) )
80 27 eqcomd 
 |-  ( ph -> ( Y .- C ) = ( Y .- D ) )
81 eqidd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` Z ) ` Q ) = ( ( ( pInvG ` G ) ` Z ) ` Q ) )
82 1 2 3 4 38 5 46 47 23 48 13 7 15 14 12 53 26 79 80 81 28 krippen 
 |-  ( ph -> Y e. ( Z I X ) )
83 1 3 4 5 14 13 12 45 82 btwnlng3 
 |-  ( ph -> X e. ( Z L Y ) )
84 1 3 4 5 13 14 12 44 83 lncom 
 |-  ( ph -> X e. ( Y L Z ) )
85 19 eqcomd 
 |-  ( ph -> ( E .- C ) = ( E .- Y ) )
86 1 2 3 5 9 7 9 13 85 64 tgcgrneq 
 |-  ( ph -> E =/= Y )
87 1 3 4 5 9 13 14 86 21 btwnlng3 
 |-  ( ph -> Z e. ( E L Y ) )
88 1 3 4 5 9 13 86 86 6 62 33 tglinethru 
 |-  ( ph -> A = ( E L Y ) )
89 87 88 eleqtrrd 
 |-  ( ph -> Z e. A )
90 1 3 4 5 13 14 44 44 6 33 89 tglinethru 
 |-  ( ph -> A = ( Y L Z ) )
91 84 90 eleqtrrd 
 |-  ( ph -> X e. A )