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

Theorem opphllem3 24791
 Description: Lemma for opphl 24796: 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 hlG
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 hlG
4 opphllem3.u . . . . . 6
54ad4antr 738 . . . . 5
6 opphllem5.a . . . . . 6
76ad4antr 738 . . . . 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 24594 . . . . . 6
1312ad4antr 738 . . . . 5
149ad4antr 738 . . . . 5 TarskiG
15 simplr 762 . . . . 5
16 simprl 764 . . . . 5
17 opphllem5.p . . . . . . . 8 ⟂G
188, 9, 17perpln2 24756 . . . . . . 7
191, 2, 8, 9, 6, 12, 18tglnne 24673 . . . . . 6
2019ad4antr 738 . . . . 5
21 hpg.d . . . . . 6
22 opphllem5.c . . . . . . 7
2322ad4antr 738 . . . . . 6
24 opphllem5.s . . . . . . . 8
251, 8, 2, 9, 10, 24tglnpt 24594 . . . . . . 7
2625ad4antr 738 . . . . . 6
27 simprr 766 . . . . . . 7
281, 21, 2, 14, 26, 23, 13, 15, 27tgcgrcomlr 24524 . . . . . 6
29 opphllem5.q . . . . . . . . 9 ⟂G
3029ad4antr 738 . . . . . . . 8 ⟂G
318, 14, 30perpln2 24756 . . . . . . 7
321, 2, 8, 14, 23, 26, 31tglnne 24673 . . . . . 6
331, 21, 2, 14, 23, 26, 15, 13, 28, 32tgcgrneq 24527 . . . . 5
341, 2, 3, 5, 7, 13, 14, 15, 16, 20, 33hlbtwn 24656 . . . 4
35 eqid 2451 . . . . . . 7 pInvG pInvG
3614adantr 467 . . . . . . 7 TarskiG
37 opphllem5.n . . . . . . 7 pInvG
38 opphllem5.m . . . . . . . 8
3938ad5antr 740 . . . . . . 7
405adantr 467 . . . . . . 7
4115adantr 467 . . . . . . 7
4213adantr 467 . . . . . . 7
43 simpr 463 . . . . . . 7
441, 21, 2, 8, 35, 36, 37, 3, 39, 40, 41, 42, 43mirhl 24724 . . . . . 6
45 eqidd 2452 . . . . . . 7
46 opphllem3.v . . . . . . . . 9
4746ad5antr 740 . . . . . . . 8
4847fveq2d 5869 . . . . . . 7
49 simprr 766 . . . . . . . . . 10 pInvG pInvG pInvG
5014ad2antrr 732 . . . . . . . . . . . . . 14 pInvG pInvG TarskiG
51 simplr 762 . . . . . . . . . . . . . 14 pInvG pInvG
5238ad6antr 742 . . . . . . . . . . . . . 14 pInvG pInvG
5326ad2antrr 732 . . . . . . . . . . . . . 14 pInvG pInvG
5413ad2antrr 732 . . . . . . . . . . . . . 14 pInvG pInvG
55 simprl 764 . . . . . . . . . . . . . . 15 pInvG pInvG pInvG
5655eqcomd 2457 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
5737fveq1i 5866 . . . . . . . . . . . . . . . 16 pInvG
581, 21, 2, 8, 35, 9, 38, 37, 12, 46mircom 24708 . . . . . . . . . . . . . . . 16
5957, 58syl5eqr 2499 . . . . . . . . . . . . . . 15 pInvG
6059ad6antr 742 . . . . . . . . . . . . . 14 pInvG pInvG pInvG
611, 21, 2, 8, 35, 50, 51, 52, 53, 54, 56, 60miduniq 24730 . . . . . . . . . . . . 13 pInvG pInvG
6261fveq2d 5869 . . . . . . . . . . . 12 pInvG pInvG pInvG pInvG
6362, 37syl6eqr 2503 . . . . . . . . . . 11 pInvG pInvG pInvG
6463fveq1d 5867 . . . . . . . . . 10 pInvG pInvG pInvG
6549, 64eqtr2d 2486 . . . . . . . . 9 pInvG pInvG
66 opphllem3.t . . . . . . . . . . . 12
6766ad4antr 738 . . . . . . . . . . 11
6867necomd 2679 . . . . . . . . . 10
6910ad4antr 738 . . . . . . . . . . 11
70 simp-4r 777 . . . . . . . . . . 11
711, 8, 2, 14, 69, 70tglnpt 24594 . . . . . . . . . 10
7224ad4antr 738 . . . . . . . . . . . 12
7311ad4antr 738 . . . . . . . . . . . 12
741, 2, 8, 14, 26, 13, 68, 68, 69, 72, 73tglinethru 24681 . . . . . . . . . . 11
7517ad4antr 738 . . . . . . . . . . 11 ⟂G
7674, 75eqbrtrrd 4425 . . . . . . . . . 10 ⟂G
771, 2, 8, 14, 23, 26, 32tglinecom 24680 . . . . . . . . . . 11
7830, 74, 773brtr3d 4432 . . . . . . . . . 10 ⟂G
7970, 74eleqtrd 2531 . . . . . . . . . 10
80 simpllr 769 . . . . . . . . . 10
811, 21, 2, 8, 14, 35, 26, 13, 68, 7, 23, 71, 76, 78, 79, 80, 15, 16, 27opphllem 24777 . . . . . . . . 9 pInvG pInvG
8265, 81r19.29a 2932 . . . . . . . 8
8382adantr 467 . . . . . . 7
8445, 48, 83breq123d 4416 . . . . . 6
8544, 84mpbid 214 . . . . 5
8614adantr 467 . . . . . . 7 TarskiG
8738ad5antr 740 . . . . . . 7
881, 21, 2, 8, 35, 9, 38, 37, 4mircl 24706 . . . . . . . 8
8988ad5antr 740 . . . . . . 7
9023adantr 467 . . . . . . 7
9126adantr 467 . . . . . . 7
92 simpr 463 . . . . . . 7
931, 21, 2, 8, 35, 86, 37, 3, 87, 89, 90, 91, 92mirhl 24724 . . . . . 6
945adantr 467 . . . . . . . 8
951, 21, 2, 8, 35, 86, 87, 37, 94mirmir 24707 . . . . . . 7
9613adantr 467 . . . . . . . . 9
9746ad5antr 740 . . . . . . . . 9
981, 21, 2, 8, 35, 86, 87, 37, 96, 97mircom 24708 . . . . . . . 8
9998fveq2d 5869 . . . . . . 7
10015adantr 467 . . . . . . . 8
10182adantr 467 . . . . . . . 8
1021, 21, 2, 8, 35, 86, 87, 37, 100, 101mircom 24708 . . . . . . 7
10395, 99, 102breq123d 4416 . . . . . 6
10493, 103mpbid 214 . . . . 5
10585, 104impbida 843 . . . 4
10634, 105bitrd 257 . . 3
107 opphllem3.l . . . . 5 ≤G
108 eqid 2451 . . . . . 6 ≤G ≤G
1091, 21, 2, 108, 9, 25, 22, 12, 6legov 24630 . . . . 5 ≤G
110107, 109mpbid 214 . . . 4