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

Theorem mideulem 23841
 Description: Lemma for mideu 23842. We can assume mideulem.9 "without loss of generality" (Contributed by Thierry Arnoux, 25-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p
colperpex.d
colperpex.i Itv
colperpex.l LineG
colperpex.g TarskiG
mideu.s pInvG
mideu.1
mideu.2
mideulem.1
mideulem.2
mideulem.3
mideulem.4
mideulem.5 ⟂G
mideulem.6 ⟂G
mideulem.7
mideulem.8
mideulem.9 ≤G
Assertion
Ref Expression
mideulem
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem mideulem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 colperpex.p . . . 4
2 colperpex.d . . . 4
3 colperpex.i . . . 4 Itv
4 colperpex.l . . . 4 LineG
5 mideu.s . . . 4 pInvG
6 colperpex.g . . . . . 6 TarskiG
76ad2antrr 725 . . . . 5 TarskiG
87adantr 465 . . . 4 TarskiG
9 eqid 2467 . . . 4
10 mideu.2 . . . . . 6
1110ad2antrr 725 . . . . 5
1211adantr 465 . . . 4
13 mideulem.3 . . . . . 6
1413ad2antrr 725 . . . . 5
1514adantr 465 . . . 4
16 mideu.1 . . . . 5
1716ad3antrrr 729 . . . 4
18 simplr 754 . . . . 5
1918adantr 465 . . . 4
20 simprl 755 . . . 4
21 mideulem.1 . . . . . . . . . . . . . . 15
2221necomd 2738 . . . . . . . . . . . . . 14
2322neneqd 2669 . . . . . . . . . . . . 13
2423adantr 465 . . . . . . . . . . . 12
25 mideulem.6 . . . . . . . . . . . . . . . . 17 ⟂G
264, 6, 25perpln2 23824 . . . . . . . . . . . . . . . 16
271, 3, 4, 6, 16, 13, 26tglnne 23750 . . . . . . . . . . . . . . 15
2827necomd 2738 . . . . . . . . . . . . . 14
2928neneqd 2669 . . . . . . . . . . . . 13
3029adantr 465 . . . . . . . . . . . 12
3124, 30jca 532 . . . . . . . . . . 11
326adantr 465 . . . . . . . . . . . . 13 TarskiG
3310adantr 465 . . . . . . . . . . . . 13
3416adantr 465 . . . . . . . . . . . . 13
3513adantr 465 . . . . . . . . . . . . 13
361, 3, 4, 6, 10, 16, 22tglinerflx2 23756 . . . . . . . . . . . . . . 15
371, 3, 4, 6, 16, 10, 21tglinecom 23757 . . . . . . . . . . . . . . . 16
3837, 25eqbrtrrd 4469 . . . . . . . . . . . . . . 15 ⟂G
391, 2, 3, 4, 6, 10, 16, 36, 13, 38perprag 23833 . . . . . . . . . . . . . 14 ∟G
4039adantr 465 . . . . . . . . . . . . 13 ∟G
41 simpr 461 . . . . . . . . . . . . . 14
4241orcd 392 . . . . . . . . . . . . 13
431, 2, 3, 4, 5, 32, 33, 34, 35, 40, 42ragflat3 23819 . . . . . . . . . . . 12
44 oran 496 . . . . . . . . . . . 12
4543, 44sylib 196 . . . . . . . . . . 11
4631, 45pm2.65da 576 . . . . . . . . . 10
4746ad2antrr 725 . . . . . . . . 9
4847adantr 465 . . . . . . . 8
4937ad3antrrr 729 . . . . . . . 8
5048, 49neleqtrrd 2580 . . . . . . 7
5121ad3antrrr 729 . . . . . . . 8
5251neneqd 2669 . . . . . . 7
5350, 52jca 532 . . . . . 6
54 pm4.56 495 . . . . . 6
5553, 54sylib 196 . . . . 5
561, 4, 3, 8, 17, 12, 15, 55ncolrot2 23706 . . . 4
57 simprrr 764 . . . . . 6
581, 2, 3, 8, 19, 20, 15, 57tgbtwncom 23635 . . . . 5
59 mideulem.4 . . . . . . . . 9
6059ad2antrr 725 . . . . . . . 8
6160adantr 465 . . . . . . 7
62 mideulem.7 . . . . . . . 8
6362ad3antrrr 729 . . . . . . 7
64 simprrl 763 . . . . . . 7
651, 3, 4, 8, 61, 17, 12, 20, 63, 64coltr3 23770 . . . . . 6
6637ad2antrr 725 . . . . . . . 8
6747, 66neleqtrrd 2580 . . . . . . 7
6867adantr 465 . . . . . 6
69 nelne2 2797 . . . . . 6
7065, 68, 69syl2anc 661 . . . . 5
711, 2, 3, 8, 15, 20, 19, 58, 70tgbtwnne 23637 . . . 4
721, 2, 3, 4, 5, 6, 10, 16, 13israg 23810 . . . . . . . 8 ∟G
7339, 72mpbid 210 . . . . . . 7
7473ad5antr 733 . . . . . 6
758ad2antrr 725 . . . . . . 7 TarskiG
76 eqid 2467 . . . . . . . . 9
771, 2, 3, 4, 5, 8, 17, 76, 15mircl 23783 . . . . . . . 8
7877ad2antrr 725 . . . . . . 7
7917ad2antrr 725 . . . . . . 7
8015ad2antrr 725 . . . . . . 7
8119ad2antrr 725 . . . . . . 7
8212ad2antrr 725 . . . . . . 7
83 simplr 754 . . . . . . 7
841, 2, 3, 4, 5, 75, 79, 76, 80mirbtwn 23780 . . . . . . 7
85 eqid 2467 . . . . . . . . 9
861, 2, 3, 4, 5, 75, 82, 85, 83mirbtwn 23780 . . . . . . . 8
87 simpr 461 . . . . . . . . . . 11
88 oveq2 6292 . . . . . . . . . . . . . . . 16
8988breq1d 4457 . . . . . . . . . . . . . . 15 ⟂G ⟂G
90 oveq2 6292 . . . . . . . . . . . . . . . 16
9190breq1d 4457 . . . . . . . . . . . . . . 15 ⟂G ⟂G
9275ad2antrr 725 . . . . . . . . . . . . . . . 16 TarskiG
931, 3, 4, 6, 16, 10, 21tgelrnln 23752 . . . . . . . . . . . . . . . . 17
9493ad7antr 737 . . . . . . . . . . . . . . . 16
9581ad2antrr 725 . . . . . . . . . . . . . . . 16
9621ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20
9796neneqd 2669 . . . . . . . . . . . . . . . . . . 19
9816ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
99 simprr 756 . . . . . . . . . . . . . . . . . . . . . . 23
10027ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
1011, 2, 3, 7, 98, 14, 11, 18, 99, 100tgcgrneq 23630 . . . . . . . . . . . . . . . . . . . . . 22
102101adantr 465 . . . . . . . . . . . . . . . . . . . . 21
103102necomd 2738 . . . . . . . . . . . . . . . . . . . 20
104103neneqd 2669 . . . . . . . . . . . . . . . . . . 19
10597, 104jca 532 . . . . . . . . . . . . . . . . . 18
1067adantr 465 . . . . . . . . . . . . . . . . . . . 20 TarskiG
10716ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20
10811adantr 465 . . . . . . . . . . . . . . . . . . . 20
10918adantr 465 . . . . . . . . . . . . . . . . . . . 20
110 mideulem.2 . . . . . . . . . . . . . . . . . . . . . . . 24
111110ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
112 mideulem.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⟂G
1134, 6, 112perpln2 23824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1141, 3, 4, 6, 110, 10, 113tglnne 23750 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1151, 3, 4, 6, 110, 10, 114tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . . . . . 25
1161, 2, 3, 4, 6, 93, 113, 112perpcom 23826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⟂G
117116, 37breqtrd 4471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⟂G
1181, 2, 3, 4, 6, 110, 10, 115, 16, 117perprag 23833 . . . . . . . . . . . . . . . . . . . . . . . 24 ∟G
119118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ∟G
120114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
121 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . 24
1221, 4, 3, 7, 11, 18, 111, 121btwncolg3 23700 . . . . . . . . . . . . . . . . . . . . . . 23
1231, 2, 3, 4, 5, 7, 111, 11, 98, 18, 119, 120, 122ragcol 23812 . . . . . . . . . . . . . . . . . . . . . 22 ∟G
1241, 2, 3, 4, 5, 7, 18, 11, 98, 123ragcom 23811 . . . . . . . . . . . . . . . . . . . . 21 ∟G
125124adantr 465 . . . . . . . . . . . . . . . . . . . 20 ∟G
126 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
127126orcd 392 . . . . . . . . . . . . . . . . . . . 20
1281, 2, 3, 4, 5, 106, 107, 108, 109, 125, 127ragflat3 23819 . . . . . . . . . . . . . . . . . . 19
129 oran 496 . . . . . . . . . . . . . . . . . . 19
130128, 129sylib 196 . . . . . . . . . . . . . . . . . 18
131105, 130pm2.65da 576 . . . . . . . . . . . . . . . . 17
132131ad5antr 733 . . . . . . . . . . . . . . . 16
1331, 2, 3, 4, 92, 94, 95, 132foot 23832 . . . . . . . . . . . . . . 15 ⟂G
13479ad2antrr 725 . . . . . . . . . . . . . . . 16
13582ad2antrr 725 . . . . . . . . . . . . . . . 16
13651ad4antr 731 . . . . . . . . . . . . . . . 16
1371, 3, 4, 92, 134, 135, 136tglinerflx2 23756 . . . . . . . . . . . . . . 15
13820ad2antrr 725 . . . . . . . . . . . . . . . . 17
139138ad2antrr 725 . . . . . . . . . . . . . . . 16
140 oveq2 6292 . . . . . . . . . . . . . . . . . . . . 21
141140breq1d 4457 . . . . . . . . . . . . . . . . . . . 20 ⟂G ⟂G
14293ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22
1431, 2, 3, 4, 7, 142, 18, 131foot 23832 . . . . . . . . . . . . . . . . . . . . 21 ⟂G
144143ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ⟂G
14521ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22
1461, 3, 4, 7, 98, 11, 145tglinerflx1 23755 . . . . . . . . . . . . . . . . . . . . 21
147146ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
1481, 3, 4, 7, 98, 11, 145tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . 21
149148ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
1508adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 TarskiG
15118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
15217adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
153145neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
154131, 153jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
155 pm4.56 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
156154, 155sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1571, 3, 4, 7, 18, 98, 11, 156ncolne1 23747 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158157ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
159158necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . 24
160159necomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23
1611, 3, 4, 150, 151, 152, 160tglinecom 23757 . . . . . . . . . . . . . . . . . . . . . 22
16214ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
16328ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . 23
16420adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
165 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166165, 159eqnetrd 2760 . . . . . . . . . . . . . . . . . . . . . . . . 25
16771adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
168167necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26
169 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170169simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1711, 3, 4, 150, 151, 162, 164, 168, 170btwnlng1 23741 . . . . . . . . . . . . . . . . . . . . . . . . 25
1721, 3, 4, 150, 164, 151, 162, 166, 171, 168lnrot2 23746 . . . . . . . . . . . . . . . . . . . . . . . 24
173165oveq1d 6299 . . . . . . . . . . . . . . . . . . . . . . . 24
174172, 173eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . 23
1751, 3, 4, 150, 152, 151, 159, 162, 163, 174tglineelsb2 23754 . . . . . . . . . . . . . . . . . . . . . 22
176161, 175eqtrd 2508 . . . . . . . . . . . . . . . . . . . . 21
1771, 2, 3, 4, 6, 93, 26, 25perpcom 23826 . . . . . . . . . . . . . . . . . . . . . 22 ⟂G
178177ad4antr 731 . . . . . . . . . . . . . . . . . . . . 21 ⟂G
179176, 178eqbrtrd 4467 . . . . . . . . . . . . . . . . . . . 20 ⟂G
180142ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
181101necomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23
1821, 3, 4, 7, 18, 11, 181tgelrnln 23752 . . . . . . . . . . . . . . . . . . . . . 22
183182ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
1841, 3, 4, 7, 18, 11, 181tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . . . . 24
185148, 184elind 3688 . . . . . . . . . . . . . . . . . . . . . . 23
1861, 3, 4, 7, 18, 11, 181tglinerflx1 23755 . . . . . . . . . . . . . . . . . . . . . . 23
1871, 2, 3, 4, 7, 142, 182, 185, 146, 186, 145, 181, 124ragperp 23830 . . . . . . . . . . . . . . . . . . . . . 22 ⟂G
188187ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ⟂G
1891, 2, 3, 4, 150, 180, 183, 188perpcom 23826 . . . . . . . . . . . . . . . . . . . 20 ⟂G
190141, 89, 144, 147, 149, 179, 189reu2eqd 3300 . . . . . . . . . . . . . . . . . . 19
19151adantr 465 . . . . . . . . . . . . . . . . . . . 20
192191neneqd 2669 . . . . . . . . . . . . . . . . . . 19
193190, 192pm2.65da 576 . . . . . . . . . . . . . . . . . 18
194193neqned 2670 . . . . . . . . . . . . . . . . 17
195194ad4antr 731 . . . . . . . . . . . . . . . 16
19665ad2antrr 725 . . . . . . . . . . . . . . . . 17
197196ad2antrr 725 . . . . . . . . . . . . . . . 16
198 simplr 754 . . . . . . . . . . . . . . . 16
199195necomd 2738 . . . . . . . . . . . . . . . . 17
200 eqid 2467 . . . . . . . . . . . . . . . . . 18
20180ad2antrr 725 . . . . . . . . . . . . . . . . . 18
20277ad4antr 731 . . . . . . . . . . . . . . . . . 18
20383ad2antrr 725 . . . . . . . . . . . . . . . . . 18
204 simp-5r 768 . . . . . . . . . . . . . . . . . . . . 21
205204simprd 463 . . . . . . . . . . . . . . . . . . . 20
206205simprd 463 . . . . . . . . . . . . . . . . . . 19
2071, 2, 3, 92, 95, 139, 201, 206tgbtwncom 23635 . . . . . . . . . . . . . . . . . 18
208 simpllr 758 . . . . . . . . . . . . . . . . . . 19
209208simpld 459 . . . . . . . . . . . . . . . . . 18
21039ad5antr 733 . . . . . . . . . . . . . . . . . . . . 21 ∟G
21151necomd 2738 . . . . . . . . . . . . . . . . . . . . . 22
212211ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
213196orcd 392 . . . . . . . . . . . . . . . . . . . . . . 23
2141, 4, 3, 75, 79, 82, 138, 213colcom 23701 . . . . . . . . . . . . . . . . . . . . . 22
2151, 4, 3, 75, 82, 79, 138, 214colrot1 23702 . . . . . . . . . . . . . . . . . . . . 21
2161, 2, 3, 4, 5, 75, 82, 79, 80, 138, 210, 212, 215ragcol 23812 . . . . . . . . . . . . . . . . . . . 20 ∟G
2171, 2, 3, 4, 5, 75, 138, 79, 80israg 23810 . . . . . . . . . . . . . . . . . . . 20 ∟G
218216, 217mpbid 210 . . . . . . . . . . . . . . . . . . 19
219218ad2antrr 725 . . . . . . . . . . . . . . . . . 18
220 simprr 756 . . . . . . . . . . . . . . . . . . . 20
221220ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
222221eqcomd 2475 . . . . . . . . . . . . . . . . . 18
223 eqidd 2468 . . . . . . . . . . . . . . . . . 18
22487eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20
2251, 2, 3, 4, 5, 92, 198, 200, 203, 224mircom 23785 . . . . . . . . . . . . . . . . . . 19
226225eqcomd 2475 . . . . . . . . . . . . . . . . . 18
2271, 2, 3, 4, 5, 92, 76, 200, 201, 202, 139, 95, 203, 134, 198, 207, 209, 219, 222, 223, 226krippen 23804 . . . . . . . . . . . . . . . . 17
2281, 3, 4, 92, 134, 139, 198, 199, 227btwnlng3 23743 . . . . . . . . . . . . . . . 16
2291, 3, 4, 92, 134, 135, 136, 139, 195, 197, 198, 228tglineeltr 23753 . . . . . . . . . . . . . . 15
230182ad5antr 733 . . . . . . . . . . . . . . . 16
231187ad5antr 733 . . . . . . . . . . . . . . . 16 ⟂G
2321, 2, 3, 4, 92, 94, 230, 231perpcom 23826 . . . . . . . . . . . . . . 15 ⟂G
233 nelne2 2797 . . . . . . . . . . . . . . . . . . 19
234229, 132, 233syl2anc 661 . . . . . . . . . . . . . . . . . 18
235234necomd 2738 . . . . . . . . . . . . . . . . 17
2361, 3, 4, 92, 95, 198, 235tgelrnln 23752 . . . . . . . . . . . . . . . 16
2371, 3, 4, 92, 95, 198, 235tglinerflx2 23756 . . . . . . . . . . . . . . . . . 18
238229, 237elind 3688 . . . . . . . . . . . . . . . . 17
2391, 3, 4, 92, 95, 198, 235tglinerflx1 23755 . . . . . . . . . . . . . . . . 17
240 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
24192adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 TarskiG
242198adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
243134adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
244201adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
245202adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
246219adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25