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

Theorem opphllem3 24338
 Description: Lemma for opphl 24342: We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020.)
Hypotheses
Ref Expression
hpg.p
hpg.d
hpg.i Itv
hpg.o
opphl.l LineG
opphl.d
opphl.g TarskiG
opphl.k
opphllem5.n pInvG
opphllem5.a
opphllem5.c
opphllem5.r
opphllem5.s
opphllem5.m
opphllem5.o
opphllem5.p ⟂G
opphllem5.q ⟂G
opphllem3.t
opphllem3.l ≤G
opphllem3.u
opphllem3.v
Assertion
Ref Expression
opphllem3
Distinct variable groups:   ,,,,   ,,,   ,,,,   ,,,,   ,,,   ,,,,   ,   ,,,,   ,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   (,,)   ()   ()   (,,)

Proof of Theorem opphllem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hpg.p . . . . 5
2 hpg.i . . . . 5 Itv
3 opphl.k . . . . 5
4 opphllem3.u . . . . . 6
54ad4antr 731 . . . . 5
6 opphllem5.a . . . . . 6
76ad4antr 731 . . . . 5
8 opphl.l . . . . . . 7 LineG
9 opphl.g . . . . . . 7 TarskiG
10 opphl.d . . . . . . 7
11 opphllem5.r . . . . . . 7
121, 8, 2, 9, 10, 11tglnpt 24153 . . . . . 6
1312ad4antr 731 . . . . 5
149ad4antr 731 . . . . 5 TarskiG
15 simplr 755 . . . . 5
16 simprl 756 . . . . 5
17 opphllem5.p . . . . . . . 8 ⟂G
188, 9, 17perpln2 24305 . . . . . . 7
191, 2, 8, 9, 6, 12, 18tglnne 24225 . . . . . 6
2019ad4antr 731 . . . . 5
21 hpg.d . . . . . 6
22 opphllem5.c . . . . . . 7
2322ad4antr 731 . . . . . 6
24 opphllem5.s . . . . . . . 8
251, 8, 2, 9, 10, 24tglnpt 24153 . . . . . . 7
2625ad4antr 731 . . . . . 6
27 simprr 757 . . . . . . 7
281, 21, 2, 14, 26, 23, 13, 15, 27tgcgrcomlr 24088 . . . . . 6
29 opphllem5.q . . . . . . . . 9 ⟂G
3029ad4antr 731 . . . . . . . 8 ⟂G
318, 14, 30perpln2 24305 . . . . . . 7
321, 2, 8, 14, 23, 26, 31tglnne 24225 . . . . . 6
331, 21, 2, 14, 23, 26, 15, 13, 28, 32tgcgrneq 24091 . . . . 5
341, 2, 3, 5, 7, 13, 14, 15, 16, 20, 33hlbtwn 24212 . . . 4
35 eqid 2457 . . . . . . 7 pInvG pInvG
3614adantr 465 . . . . . . 7 TarskiG
37 opphllem5.n . . . . . . 7 pInvG
38 opphllem5.m . . . . . . . 8
3938ad5antr 733 . . . . . . 7
405adantr 465 . . . . . . 7
4115adantr 465 . . . . . . 7
4213adantr 465 . . . . . . 7
43 simpr 461 . . . . . . 7
441, 21, 2, 8, 35, 36, 37, 3, 39, 40, 41, 42, 43mirhl 24276 . . . . . 6
45 eqidd 2458 . . . . . . 7
46 opphllem3.v . . . . . . . . 9
4746ad5antr 733 . . . . . . . 8
4847fveq2d 5876 . . . . . . 7
49 simprr 757 . . . . . . . . . 10 pInvG pInvG pInvG
5014ad2antrr 725 . . . . . . . . . . . . . 14 pInvG pInvG TarskiG
51 simplr 755 . . . . . . . . . . . . . 14 pInvG pInvG
5238ad6antr 735 . . . . . . . . . . . . . 14 pInvG pInvG
5326ad2antrr 725 . . . . . . . . . . . . . 14 pInvG pInvG
5413ad2antrr 725 . . . . . . . . . . . . . 14 pInvG pInvG
55 simprl 756 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
5655eqcomd 2465 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
5737fveq1i 5873 . . . . . . . . . . . . . . . 16 pInvG
581, 21, 2, 8, 35, 9, 38, 37, 12, 46mircom 24261 . . . . . . . . . . . . . . . 16
5957, 58syl5eqr 2512 . . . . . . . . . . . . . . 15 pInvG
6059ad6antr 735 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
611, 21, 2, 8, 35, 50, 51, 52, 53, 54, 56, 60miduniq 24279 . . . . . . . . . . . . 13 pInvG pInvG
6261fveq2d 5876 . . . . . . . . . . . 12 pInvG pInvG pInvG pInvG
6362, 37syl6eqr 2516 . . . . . . . . . . 11 pInvG pInvG pInvG
6463fveq1d 5874 . . . . . . . . . 10 pInvG pInvG pInvG
6549, 64eqtr2d 2499 . . . . . . . . 9 pInvG pInvG
66 opphllem3.t . . . . . . . . . . . 12
6766ad4antr 731 . . . . . . . . . . 11
6867necomd 2728 . . . . . . . . . 10
6910ad4antr 731 . . . . . . . . . . 11
70 simp-4r 768 . . . . . . . . . . 11
711, 8, 2, 14, 69, 70tglnpt 24153 . . . . . . . . . 10
7224ad4antr 731 . . . . . . . . . . . 12
7311ad4antr 731 . . . . . . . . . . . 12
741, 2, 8, 14, 26, 13, 68, 68, 69, 72, 73tglinethru 24233 . . . . . . . . . . 11
7517ad4antr 731 . . . . . . . . . . 11 ⟂G
7674, 75eqbrtrrd 4478 . . . . . . . . . 10 ⟂G
771, 2, 8, 14, 23, 26, 32tglinecom 24232 . . . . . . . . . . 11
7830, 74, 773brtr3d 4485 . . . . . . . . . 10 ⟂G
7970, 74eleqtrd 2547 . . . . . . . . . 10
80 simpllr 760 . . . . . . . . . 10
811, 21, 2, 8, 14, 35, 26, 13, 68, 7, 23, 71, 76, 78, 79, 80, 15, 16, 27opphllem 24326 . . . . . . . . 9 pInvG pInvG
8265, 81r19.29a 2999 . . . . . . . 8
8382adantr 465 . . . . . . 7
8445, 48, 83breq123d 4470 . . . . . 6
8544, 84mpbid 210 . . . . 5
8614adantr 465 . . . . . . 7 TarskiG
8738ad5antr 733 . . . . . . 7
881, 21, 2, 8, 35, 9, 38, 37, 4mircl 24259 . . . . . . . 8
8988ad5antr 733 . . . . . . 7
9023adantr 465 . . . . . . 7
9126adantr 465 . . . . . . 7
92 simpr 461 . . . . . . 7
931, 21, 2, 8, 35, 86, 37, 3, 87, 89, 90, 91, 92mirhl 24276 . . . . . 6
945adantr 465 . . . . . . . 8
951, 21, 2, 8, 35, 86, 87, 37, 94mirmir 24260 . . . . . . 7
9613adantr 465 . . . . . . . . 9
9746ad5antr 733 . . . . . . . . 9
981, 21, 2, 8, 35, 86, 87, 37, 96, 97mircom 24261 . . . . . . . 8
9998fveq2d 5876 . . . . . . 7
10015adantr 465 . . . . . . . 8
10182adantr 465 . . . . . . . 8
1021, 21, 2, 8, 35, 86, 87, 37, 100, 101mircom 24261 . . . . . . 7
10395, 99, 102breq123d 4470 . . . . . 6
10493, 103mpbid 210 . . . . 5
10585, 104impbida 832 . . . 4
10634, 105bitrd 253 . . 3
107 opphllem3.l . . . . 5 ≤G
108 eqid 2457 . . . . . 6 ≤G ≤G
1091, 21, 2, 108, 9, 25, 22, 12, 6legov 24189 . . . . 5 ≤G
110107, 109mpbid 210 . . . 4