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

Theorem colperpexlem2 24766
 Description: Lemma for colperpex 24768. Second part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p
colperpex.d
colperpex.i Itv
colperpex.l LineG
colperpex.g TarskiG
colperpexlem.s pInvG
colperpexlem.m
colperpexlem.n
colperpexlem.k
colperpexlem.a
colperpexlem.b
colperpexlem.c
colperpexlem.q
colperpexlem.1 ∟G
colperpexlem.2
colperpexlem2.e
Assertion
Ref Expression
colperpexlem2

Proof of Theorem colperpexlem2
StepHypRef Expression
1 colperpexlem2.e . . 3
2 simpr 463 . . . . . . . . . 10
32fveq2d 5867 . . . . . . . . 9
4 colperpexlem.m . . . . . . . . 9
5 colperpexlem.k . . . . . . . . 9
63, 4, 53eqtr4g 2509 . . . . . . . 8
76fveq1d 5865 . . . . . . 7
8 colperpex.p . . . . . . . . 9
9 colperpex.d . . . . . . . . 9
10 colperpex.i . . . . . . . . 9 Itv
11 colperpex.l . . . . . . . . 9 LineG
12 colperpexlem.s . . . . . . . . 9 pInvG
13 colperpex.g . . . . . . . . 9 TarskiG
14 colperpexlem.a . . . . . . . . 9
15 colperpexlem.c . . . . . . . . 9
168, 9, 10, 11, 12, 13, 14, 4, 15mirmir 24700 . . . . . . . 8
1716adantr 467 . . . . . . 7
18 colperpexlem.2 . . . . . . . 8
1918adantr 467 . . . . . . 7
207, 17, 193eqtr3rd 2493 . . . . . 6
21 colperpexlem.b . . . . . . . 8
22 colperpexlem.n . . . . . . . 8
238, 9, 10, 11, 12, 13, 21, 22, 15mirinv 24704 . . . . . . 7
2423adantr 467 . . . . . 6
2520, 24mpbid 214 . . . . 5
2625ex 436 . . . 4