Step | Hyp | Ref
| Expression |
1 | | lmimid.s |
. . . . . . 7
β’ π = ((pInvGβπΊ)βπ΅) |
2 | 1 | a1i 11 |
. . . . . 6
β’ (π β π = ((pInvGβπΊ)βπ΅)) |
3 | 2 | fveq1d 6849 |
. . . . 5
β’ (π β (πβπΆ) = (((pInvGβπΊ)βπ΅)βπΆ)) |
4 | | ismid.p |
. . . . . 6
β’ π = (BaseβπΊ) |
5 | | ismid.d |
. . . . . 6
β’ β =
(distβπΊ) |
6 | | ismid.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
7 | | ismid.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
8 | | ismid.1 |
. . . . . 6
β’ (π β πΊDimTarskiGβ₯2) |
9 | | lmimid.c |
. . . . . 6
β’ (π β πΆ β π) |
10 | | lmif.l |
. . . . . . 7
β’ πΏ = (LineGβπΊ) |
11 | | eqid 2737 |
. . . . . . 7
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
12 | | lmif.d |
. . . . . . . 8
β’ (π β π· β ran πΏ) |
13 | | lmimid.b |
. . . . . . . 8
β’ (π β π΅ β π·) |
14 | 4, 10, 6, 7, 12, 13 | tglnpt 27533 |
. . . . . . 7
β’ (π β π΅ β π) |
15 | 4, 5, 6, 10, 11, 7, 14, 1, 9 | mircl 27645 |
. . . . . 6
β’ (π β (πβπΆ) β π) |
16 | 4, 5, 6, 7, 8, 9, 15, 11, 14 | ismidb 27762 |
. . . . 5
β’ (π β ((πβπΆ) = (((pInvGβπΊ)βπ΅)βπΆ) β (πΆ(midGβπΊ)(πβπΆ)) = π΅)) |
17 | 3, 16 | mpbid 231 |
. . . 4
β’ (π β (πΆ(midGβπΊ)(πβπΆ)) = π΅) |
18 | 17, 13 | eqeltrd 2838 |
. . 3
β’ (π β (πΆ(midGβπΊ)(πβπΆ)) β π·) |
19 | | df-ne 2945 |
. . . . . 6
β’ (πΆ β (πβπΆ) β Β¬ πΆ = (πβπΆ)) |
20 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β πΊ β TarskiG) |
21 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β π· β ran πΏ) |
22 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΆ β (πβπΆ)) β πΆ β π) |
23 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΆ β (πβπΆ)) β (πβπΆ) β π) |
24 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ πΆ β (πβπΆ)) β πΆ β (πβπΆ)) |
25 | 4, 6, 10, 20, 22, 23, 24 | tgelrnln 27614 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β (πΆπΏ(πβπΆ)) β ran πΏ) |
26 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΆ β (πβπΆ)) β π΅ β π·) |
27 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΆ β (πβπΆ)) β π΅ β π) |
28 | 4, 5, 6, 7, 8, 9, 15 | midbtwn 27763 |
. . . . . . . . . . . 12
β’ (π β (πΆ(midGβπΊ)(πβπΆ)) β (πΆπΌ(πβπΆ))) |
29 | 17, 28 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (π β π΅ β (πΆπΌ(πβπΆ))) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΆ β (πβπΆ)) β π΅ β (πΆπΌ(πβπΆ))) |
31 | 4, 6, 10, 20, 22, 23, 27, 24, 30 | btwnlng1 27603 |
. . . . . . . . 9
β’ ((π β§ πΆ β (πβπΆ)) β π΅ β (πΆπΏ(πβπΆ))) |
32 | 26, 31 | elind 4159 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β π΅ β (π· β© (πΆπΏ(πβπΆ)))) |
33 | | lmimid.a |
. . . . . . . . 9
β’ (π β π΄ β π·) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β π΄ β π·) |
35 | 4, 6, 10, 20, 22, 23, 24 | tglinerflx1 27617 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β πΆ β (πΆπΏ(πβπΆ))) |
36 | | lmimid.d |
. . . . . . . . 9
β’ (π β π΄ β π΅) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β π΄ β π΅) |
38 | 4, 5, 6, 10, 11, 7, 14, 1, 9 | mirinv 27650 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπΆ) = πΆ β π΅ = πΆ)) |
39 | | eqcom 2744 |
. . . . . . . . . . . . . 14
β’ (π΅ = πΆ β πΆ = π΅) |
40 | 38, 39 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ (π β ((πβπΆ) = πΆ β πΆ = π΅)) |
41 | 40 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ = π΅) β (πβπΆ) = πΆ) |
42 | 41 | eqcomd 2743 |
. . . . . . . . . . 11
β’ ((π β§ πΆ = π΅) β πΆ = (πβπΆ)) |
43 | 42 | ex 414 |
. . . . . . . . . 10
β’ (π β (πΆ = π΅ β πΆ = (πβπΆ))) |
44 | 43 | necon3d 2965 |
. . . . . . . . 9
β’ (π β (πΆ β (πβπΆ) β πΆ β π΅)) |
45 | 44 | imp 408 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β πΆ β π΅) |
46 | | lmimid.r |
. . . . . . . . 9
β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
47 | 46 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β (πβπΆ)) β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
48 | 4, 5, 6, 10, 20, 21, 25, 32, 34, 35, 37, 45, 47 | ragperp 27701 |
. . . . . . 7
β’ ((π β§ πΆ β (πβπΆ)) β π·(βGβπΊ)(πΆπΏ(πβπΆ))) |
49 | 48 | ex 414 |
. . . . . 6
β’ (π β (πΆ β (πβπΆ) β π·(βGβπΊ)(πΆπΏ(πβπΆ)))) |
50 | 19, 49 | biimtrrid 242 |
. . . . 5
β’ (π β (Β¬ πΆ = (πβπΆ) β π·(βGβπΊ)(πΆπΏ(πβπΆ)))) |
51 | 50 | orrd 862 |
. . . 4
β’ (π β (πΆ = (πβπΆ) β¨ π·(βGβπΊ)(πΆπΏ(πβπΆ)))) |
52 | 51 | orcomd 870 |
. . 3
β’ (π β (π·(βGβπΊ)(πΆπΏ(πβπΆ)) β¨ πΆ = (πβπΆ))) |
53 | | lmif.m |
. . . 4
β’ π = ((lInvGβπΊ)βπ·) |
54 | 4, 5, 6, 7, 8, 53,
10, 12, 9, 15 | islmib 27771 |
. . 3
β’ (π β ((πβπΆ) = (πβπΆ) β ((πΆ(midGβπΊ)(πβπΆ)) β π· β§ (π·(βGβπΊ)(πΆπΏ(πβπΆ)) β¨ πΆ = (πβπΆ))))) |
55 | 18, 52, 54 | mpbir2and 712 |
. 2
β’ (π β (πβπΆ) = (πβπΆ)) |
56 | 55 | eqcomd 2743 |
1
β’ (π β (πβπΆ) = (πβπΆ)) |