Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  midexlem Structured version   Visualization version   Unicode version

Theorem midexlem 24816
 Description: Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point equidistant to and This condition will be removed later. Because the operation notation midG for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation has to be used. See mideu 24859 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
Hypotheses
Ref Expression
mirval.p
mirval.d
mirval.i Itv
mirval.l LineG
mirval.s pInvG
mirval.g TarskiG
midexlem.m
midexlem.a
midexlem.b
midexlem.c
midexlem.1
Assertion
Ref Expression
midexlem
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem midexlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 midexlem.c . . . . 5
2 midexlem.m . . . . . . . . 9
3 fveq2 5879 . . . . . . . . 9
42, 3syl5eq 2517 . . . . . . . 8
54fveq1d 5881 . . . . . . 7
65eqeq2d 2481 . . . . . 6
76rspcev 3136 . . . . 5
81, 7sylan 479 . . . 4
10 midexlem.a . . . . . 6
1110adantr 472 . . . . 5
12 mirval.p . . . . . . . 8
13 mirval.d . . . . . . . 8
14 mirval.i . . . . . . . 8 Itv
15 mirval.l . . . . . . . 8 LineG
16 mirval.s . . . . . . . 8 pInvG
17 mirval.g . . . . . . . 8 TarskiG
18 eqid 2471 . . . . . . . 8
1912, 13, 14, 15, 16, 17, 10, 18mircinv 24792 . . . . . . 7
2019adantr 472 . . . . . 6
21 simpr 468 . . . . . 6
2220, 21eqtr2d 2506 . . . . 5
23 fveq2 5879 . . . . . . . . 9
242, 23syl5eq 2517 . . . . . . . 8
2524fveq1d 5881 . . . . . . 7
2625eqeq2d 2481 . . . . . 6
2726rspcev 3136 . . . . 5
2811, 22, 27syl2anc 673 . . . 4
3017adantr 472 . . . 4 TarskiG
31 eqid 2471 . . . 4
3210adantr 472 . . . 4
33 midexlem.b . . . . 5
3433adantr 472 . . . 4
351adantr 472 . . . 4
36 simpr 468 . . . 4
37 midexlem.1 . . . . 5
3837adantr 472 . . . 4
3912, 13, 14, 15, 16, 30, 31, 32, 34, 35, 36, 38colmid 24812 . . 3
409, 29, 39mpjaodan 803 . 2
4117adantr 472 . . . . . . . . . . 11 TarskiG
4241ad2antrr 740 . . . . . . . . . 10 TarskiG
4342ad2antrr 740 . . . . . . . . 9 TarskiG
4443ad2antrr 740 . . . . . . . 8 TarskiG
4544adantr 472 . . . . . . 7 TarskiG
46 simprl 772 . . . . . . 7
4710adantr 472 . . . . . . . . . . 11
4847ad2antrr 740 . . . . . . . . . 10
4948ad2antrr 740 . . . . . . . . 9
5049ad2antrr 740 . . . . . . . 8
5150adantr 472 . . . . . . 7
5233ad3antrrr 744 . . . . . . . . . 10
5352ad2antrr 740 . . . . . . . . 9
5453ad2antrr 740 . . . . . . . 8
5554adantr 472 . . . . . . 7
5645ad2antrr 740 . . . . . . . . 9 cgrG TarskiG
57 simpllr 777 . . . . . . . . . 10
5857ad2antrr 740 . . . . . . . . 9 cgrG
591adantr 472 . . . . . . . . . . . . . 14
6059ad2antrr 740 . . . . . . . . . . . . 13
6160ad2antrr 740 . . . . . . . . . . . 12
6261ad2antrr 740 . . . . . . . . . . 11
6362adantr 472 . . . . . . . . . 10
6463ad2antrr 740 . . . . . . . . 9 cgrG
6546ad2antrr 740 . . . . . . . . 9 cgrG
66 eqid 2471 . . . . . . . . 9 cgrG cgrG
6755ad2antrr 740 . . . . . . . . 9 cgrG
6851ad2antrr 740 . . . . . . . . 9 cgrG
69 simpr 468 . . . . . . . . . . 11 cgrG
7033adantr 472 . . . . . . . . . . . . . . . 16
71 simpr 468 . . . . . . . . . . . . . . . 16
7212, 14, 15, 41, 59, 47, 70, 71ncolne1 24749 . . . . . . . . . . . . . . 15
7372ad7antr 752 . . . . . . . . . . . . . 14
7473ad2antrr 740 . . . . . . . . . . . . 13 cgrG
7574adantr 472 . . . . . . . . . . . 12 cgrG
7675necomd 2698 . . . . . . . . . . 11 cgrG
7769, 76eqnetrd 2710 . . . . . . . . . 10 cgrG
7856adantr 472 . . . . . . . . . . 11 cgrG TarskiG
7958adantr 472 . . . . . . . . . . 11 cgrG
8068adantr 472 . . . . . . . . . . 11 cgrG
8164adantr 472 . . . . . . . . . . 11 cgrG
82 simplr 770 . . . . . . . . . . . . . . 15
8382ad3antrrr 744 . . . . . . . . . . . . . 14
8483ad2antrr 740 . . . . . . . . . . . . 13 cgrG
8584adantr 472 . . . . . . . . . . . 12 cgrG
8671ad9antr 756 . . . . . . . . . . . . . . . 16 cgrG
8712, 15, 14, 56, 68, 67, 64, 86ncolrot2 24687 . . . . . . . . . . . . . . 15 cgrG
8817adantr 472 . . . . . . . . . . . . . . . . . . . . 21 TarskiG
8933adantr 472 . . . . . . . . . . . . . . . . . . . . 21
9010adantr 472 . . . . . . . . . . . . . . . . . . . . 21
911adantr 472 . . . . . . . . . . . . . . . . . . . . 21
92 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
9312, 15, 14, 88, 89, 90, 91, 92colcom 24682 . . . . . . . . . . . . . . . . . . . 20
9493stoic1a 1663 . . . . . . . . . . . . . . . . . . 19
9594ad9antr 756 . . . . . . . . . . . . . . . . . 18 cgrG
9612, 14, 15, 56, 64, 67, 68, 95ncolne1 24749 . . . . . . . . . . . . . . . . 17 cgrG
9796necomd 2698 . . . . . . . . . . . . . . . 16 cgrG
98 simprl 772 . . . . . . . . . . . . . . . . . . 19
9998ad3antrrr 744 . . . . . . . . . . . . . . . . . 18
10099ad2antrr 740 . . . . . . . . . . . . . . . . 17 cgrG
10112, 14, 15, 56, 64, 67, 84, 96, 100btwnlng3 24745 . . . . . . . . . . . . . . . 16 cgrG
10212, 14, 15, 56, 67, 64, 84, 97, 101lncom 24746 . . . . . . . . . . . . . . 15 cgrG
10356adantr 472 . . . . . . . . . . . . . . . . . 18 cgrG TarskiG
10464adantr 472 . . . . . . . . . . . . . . . . . 18 cgrG
10567adantr 472 . . . . . . . . . . . . . . . . . 18 cgrG
106100adantr 472 . . . . . . . . . . . . . . . . . . 19 cgrG
107 simpr 468 . . . . . . . . . . . . . . . . . . . 20 cgrG
108107oveq2d 6324 . . . . . . . . . . . . . . . . . . 19 cgrG
109106, 108eleqtrd 2551 . . . . . . . . . . . . . . . . . 18 cgrG
11012, 13, 14, 103, 104, 105, 109axtgbtwnid 24593 . . . . . . . . . . . . . . . . 17 cgrG
11196adantr 472 . . . . . . . . . . . . . . . . . 18 cgrG
112111neneqd 2648 . . . . . . . . . . . . . . . . 17 cgrG
113110, 112pm2.65da 586 . . . . . . . . . . . . . . . 16 cgrG
114113neqned 2650 . . . . . . . . . . . . . . 15 cgrG
11512, 14, 15, 56, 67, 64, 68, 84, 87, 102, 114ncolncol 24770 . . . . . . . . . . . . . 14 cgrG
11612, 15, 14, 56, 64, 68, 84, 115ncolcom 24685 . . . . . . . . . . . . 13 cgrG
117116adantr 472 . . . . . . . . . . . 12 cgrG
118 simp-4r 785 . . . . . . . . . . . . . . . . . . . 20
119118ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
120119adantr 472 . . . . . . . . . . . . . . . . . 18
121120ad2antrr 740 . . . . . . . . . . . . . . . . 17 cgrG
122 simp-4r 785 . . . . . . . . . . . . . . . . . . . . 21
123122simprd 470 . . . . . . . . . . . . . . . . . . . 20
124123eqcomd 2477 . . . . . . . . . . . . . . . . . . 19
125124ad2antrr 740 . . . . . . . . . . . . . . . . . 18 cgrG
12612, 13, 14, 56, 68, 121, 67, 84, 125tgcgrcomlr 24603 . . . . . . . . . . . . . . . . 17 cgrG
127 simpllr 777 . . . . . . . . . . . . . . . . . . . 20
128127ad5antr 748 . . . . . . . . . . . . . . . . . . 19 cgrG
129128simprd 470 . . . . . . . . . . . . . . . . . 18 cgrG
130129necomd 2698 . . . . . . . . . . . . . . . . 17 cgrG
13112, 13, 14, 56, 121, 68, 84, 67, 126, 130tgcgrneq 24606 . . . . . . . . . . . . . . . 16 cgrG
13212, 14, 15, 56, 64, 67, 68, 84, 95, 101, 131ncolncol 24770 . . . . . . . . . . . . . . 15 cgrG
13312, 14, 15, 56, 84, 67, 68, 132ncolne2 24750 . . . . . . . . . . . . . 14 cgrG
134133necomd 2698 . . . . . . . . . . . . . . 15 cgrG
135 simp-4r 785 . . . . . . . . . . . . . . . 16 cgrG
136135simpld 466 . . . . . . . . . . . . . . 15 cgrG
13712, 14, 15, 56, 68, 84, 58, 134, 136btwnlng1 24743 . . . . . . . . . . . . . 14 cgrG
13812, 14, 15, 56, 84, 68, 58, 133, 137lncom 24746 . . . . . . . . . . . . 13 cgrG
139138adantr 472 . . . . . . . . . . . 12 cgrG
140 simpr 468 . . . . . . . . . . . 12 cgrG
14112, 14, 15, 78, 85, 80, 81, 79, 117, 139, 140ncolncol 24770 . . . . . . . . . . 11 cgrG
14212, 14, 15, 78, 79, 80, 81, 141ncolne2 24750 . . . . . . . . . 10 cgrG
14377, 142pm2.61dane 2730 . . . . . . . . 9 cgrG
144 simpllr 777 . . . . . . . . . . . 12 cgrG
145144simprd 470 . . . . . . . . . . 11 cgrG
146145simprd 470 . . . . . . . . . 10 cgrG
14712, 15, 14, 56, 58, 65, 64, 146btwncolg3 24681 . . . . . . . . 9 cgrG
148 simplr 770 . . . . . . . . . . 11 cgrG
149 simplr 770 . . . . . . . . . . . . 13
150149simprd 470 . . . . . . . . . . . 12
151150ad2antrr 740 . . . . . . . . . . 11 cgrG
152 simprl 772 . . . . . . . . . . 11 cgrG
153127simpld 466 . . . . . . . . . . . . . . . 16
154153ad2antrr 740 . . . . . . . . . . . . . . 15
155154adantr 472 . . . . . . . . . . . . . 14
15637ad8antr 754 . . . . . . . . . . . . . 14
157156eqcomd 2477 . . . . . . . . . . . . . 14
15812, 13, 14, 45, 51, 55axtgcgrrflx 24589 . . . . . . . . . . . . . 14
15912, 13, 14, 45, 63, 51, 120, 63, 55, 83, 55, 51, 73, 155, 99, 156, 124, 157, 158axtg5seg 24592 . . . . . . . . . . . . 13
16012, 13, 14, 45, 120, 55, 83, 51, 159tgcgrcomlr 24603 . . . . . . . . . . . 12
161160ad2antrr 740 . . . . . . . . . . 11 cgrG
162 simprr 774 . . . . . . . . . . . 12