Step | Hyp | Ref
| Expression |
1 | | lmieu.a |
. . . 4
β’ (π β π΄ β π) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ π΄ β π·) β π΄ β π) |
3 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β Β¬ π΄ = π) |
4 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β (π΄(midGβπΊ)π) = (π΄(midGβπΊ)π)) |
5 | | ismid.p |
. . . . . . . . . . . . . . . 16
β’ π = (BaseβπΊ) |
6 | | ismid.d |
. . . . . . . . . . . . . . . 16
β’ β =
(distβπΊ) |
7 | | ismid.i |
. . . . . . . . . . . . . . . 16
β’ πΌ = (ItvβπΊ) |
8 | | ismid.g |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ β TarskiG) |
9 | 8 | ad4antr 731 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β πΊ β TarskiG) |
10 | | ismid.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊDimTarskiGβ₯2) |
11 | 10 | ad4antr 731 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β πΊDimTarskiGβ₯2) |
12 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π΄ β π) |
13 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π β π) |
14 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
15 | 5, 6, 7, 9, 11, 12, 13 | midcl 27761 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β (π΄(midGβπΊ)π) β π) |
16 | 5, 6, 7, 9, 11, 12, 13, 14, 15 | ismidb 27762 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β (π = (((pInvGβπΊ)β(π΄(midGβπΊ)π))βπ΄) β (π΄(midGβπΊ)π) = (π΄(midGβπΊ)π))) |
17 | 4, 16 | mpbird 257 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π = (((pInvGβπΊ)β(π΄(midGβπΊ)π))βπ΄)) |
18 | 17 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π = (((pInvGβπΊ)β(π΄(midGβπΊ)π))βπ΄)) |
19 | | lmieu.l |
. . . . . . . . . . . . . . . 16
β’ πΏ = (LineGβπΊ) |
20 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β πΊ β TarskiG) |
21 | | lmieu.1 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· β ran πΏ) |
22 | 21 | ad4antr 731 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π· β ran πΏ) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π· β ran πΏ) |
24 | 12 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ β π) |
25 | 13 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π β π) |
26 | 3 | neqned 2951 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π΄ β π) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ β π) |
28 | 5, 7, 19, 20, 24, 25, 27 | tgelrnln 27614 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (π΄πΏπ) β ran πΏ) |
29 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π· β (π΄πΏπ)) |
30 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π΄ β π·) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ β π·) |
32 | 5, 7, 19, 20, 24, 25, 27 | tglinerflx1 27617 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ β (π΄πΏπ)) |
33 | 31, 32 | elind 4159 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ β (π· β© (π΄πΏπ))) |
34 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (π΄(midGβπΊ)π) β π·) |
35 | 5, 6, 7, 9, 11, 12, 13 | midbtwn 27763 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β (π΄(midGβπΊ)π) β (π΄πΌπ)) |
36 | 5, 7, 19, 9, 12, 13, 15, 26, 35 | btwnlng1 27603 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β (π΄(midGβπΊ)π) β (π΄πΏπ)) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (π΄(midGβπΊ)π) β (π΄πΏπ)) |
38 | 34, 37 | elind 4159 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (π΄(midGβπΊ)π) β (π· β© (π΄πΏπ))) |
39 | 5, 7, 19, 20, 23, 28, 29, 33, 38 | tglineineq 27627 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ = (π΄(midGβπΊ)π)) |
40 | 39 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β ((pInvGβπΊ)βπ΄) = ((pInvGβπΊ)β(π΄(midGβπΊ)π))) |
41 | 40 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (((pInvGβπΊ)βπ΄)βπ΄) = (((pInvGβπΊ)β(π΄(midGβπΊ)π))βπ΄)) |
42 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
((pInvGβπΊ)βπ΄) = ((pInvGβπΊ)βπ΄) |
43 | 5, 6, 7, 19, 14, 20, 24, 42 | mircinv 27652 |
. . . . . . . . . . . . 13
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β (((pInvGβπΊ)βπ΄)βπ΄) = π΄) |
44 | 18, 41, 43 | 3eqtr2rd 2784 |
. . . . . . . . . . . 12
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π· β (π΄πΏπ)) β π΄ = π) |
45 | 3, 44 | mtand 815 |
. . . . . . . . . . 11
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β Β¬ π· β (π΄πΏπ)) |
46 | 8 | ad5antr 733 |
. . . . . . . . . . . 12
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β πΊ β TarskiG) |
47 | 21 | ad5antr 733 |
. . . . . . . . . . . 12
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β π· β ran πΏ) |
48 | | nne 2948 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π· β (π΄πΏπ) β π· = (π΄πΏπ)) |
49 | 45, 48 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β π· = (π΄πΏπ)) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β π· = (π΄πΏπ)) |
51 | 50, 47 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β (π΄πΏπ) β ran πΏ) |
52 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β π·(βGβπΊ)(π΄πΏπ)) |
53 | 5, 6, 7, 19, 46, 47, 51, 52 | perpneq 27698 |
. . . . . . . . . . 11
β’
((((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β§ π·(βGβπΊ)(π΄πΏπ)) β π· β (π΄πΏπ)) |
54 | 45, 53 | mtand 815 |
. . . . . . . . . 10
β’
(((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β§ Β¬ π΄ = π) β Β¬ π·(βGβπΊ)(π΄πΏπ)) |
55 | 54 | ex 414 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β (Β¬ π΄ = π β Β¬ π·(βGβπΊ)(π΄πΏπ))) |
56 | 55 | con4d 115 |
. . . . . . . 8
β’ ((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β (π·(βGβπΊ)(π΄πΏπ) β π΄ = π)) |
57 | | idd 24 |
. . . . . . . 8
β’ ((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β (π΄ = π β π΄ = π)) |
58 | 56, 57 | jaod 858 |
. . . . . . 7
β’ ((((π β§ π΄ β π·) β§ π β π) β§ (π΄(midGβπΊ)π) β π·) β ((π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π) β π΄ = π)) |
59 | 58 | impr 456 |
. . . . . 6
β’ ((((π β§ π΄ β π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π΄ = π) |
60 | 59 | eqcomd 2743 |
. . . . 5
β’ ((((π β§ π΄ β π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π = π΄) |
61 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β π = π΄) |
62 | 61 | oveq2d 7378 |
. . . . . . . 8
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β (π΄(midGβπΊ)π) = (π΄(midGβπΊ)π΄)) |
63 | 5, 6, 7, 8, 10, 1,
1 | midid 27765 |
. . . . . . . . 9
β’ (π β (π΄(midGβπΊ)π΄) = π΄) |
64 | 63 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β (π΄(midGβπΊ)π΄) = π΄) |
65 | 62, 64 | eqtrd 2777 |
. . . . . . 7
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β (π΄(midGβπΊ)π) = π΄) |
66 | | simpllr 775 |
. . . . . . 7
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β π΄ β π·) |
67 | 65, 66 | eqeltrd 2838 |
. . . . . 6
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β (π΄(midGβπΊ)π) β π·) |
68 | 61 | eqcomd 2743 |
. . . . . . 7
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β π΄ = π) |
69 | 68 | olcd 873 |
. . . . . 6
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) |
70 | 67, 69 | jca 513 |
. . . . 5
β’ ((((π β§ π΄ β π·) β§ π β π) β§ π = π΄) β ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
71 | 60, 70 | impbida 800 |
. . . 4
β’ (((π β§ π΄ β π·) β§ π β π) β (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = π΄)) |
72 | 71 | ralrimiva 3144 |
. . 3
β’ ((π β§ π΄ β π·) β βπ β π (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = π΄)) |
73 | | reu6i 3691 |
. . 3
β’ ((π΄ β π β§ βπ β π (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = π΄)) β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
74 | 2, 72, 73 | syl2anc 585 |
. 2
β’ ((π β§ π΄ β π·) β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
75 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β πΊ β TarskiG) |
76 | 75 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β πΊ β TarskiG) |
77 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ π΄ β π·) β π· β ran πΏ) |
78 | 77 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β π· β ran πΏ) |
79 | | simplr 768 |
. . . . . 6
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β π₯ β π·) |
80 | 5, 19, 7, 76, 78, 79 | tglnpt 27533 |
. . . . 5
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β π₯ β π) |
81 | | eqid 2737 |
. . . . 5
β’
((pInvGβπΊ)βπ₯) = ((pInvGβπΊ)βπ₯) |
82 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β π·) β π΄ β π) |
83 | 82 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β π΄ β π) |
84 | 5, 6, 7, 19, 14, 76, 80, 81, 83 | mircl 27645 |
. . . 4
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β (((pInvGβπΊ)βπ₯)βπ΄) β π) |
85 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π₯ = (π΄(midGβπΊ)π) β (π΄πΏπ₯) = (π΄πΏ(π΄(midGβπΊ)π))) |
86 | 85 | breq1d 5120 |
. . . . . . . . 9
β’ (π₯ = (π΄(midGβπΊ)π) β ((π΄πΏπ₯)(βGβπΊ)π· β (π΄πΏ(π΄(midGβπΊ)π))(βGβπΊ)π·)) |
87 | | simprl 770 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) β π·) |
88 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π΄ β π·) β Β¬ π΄ β π·) |
89 | 5, 6, 7, 19, 75, 77, 82, 88 | foot 27706 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π΄ β π·) β β!π₯ β π· (π΄πΏπ₯)(βGβπΊ)π·) |
90 | | reurmo 3359 |
. . . . . . . . . . 11
β’
(β!π₯ β
π· (π΄πΏπ₯)(βGβπΊ)π· β β*π₯ β π· (π΄πΏπ₯)(βGβπΊ)π·) |
91 | 89, 90 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π΄ β π·) β β*π₯ β π· (π΄πΏπ₯)(βGβπΊ)π·) |
92 | 91 | ad4antr 731 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β β*π₯ β π· (π΄πΏπ₯)(βGβπΊ)π·) |
93 | 79 | ad2antrr 725 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π₯ β π·) |
94 | | simpllr 775 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄πΏπ₯)(βGβπΊ)π·) |
95 | 76 | ad2antrr 725 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β πΊ β TarskiG) |
96 | 83 | ad2antrr 725 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π΄ β π) |
97 | | simplr 768 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π β π) |
98 | 10 | ad5antr 733 |
. . . . . . . . . . . . 13
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β πΊDimTarskiGβ₯2) |
99 | 5, 6, 7, 95, 98, 96, 97 | midcl 27761 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) β π) |
100 | 5, 6, 7, 95, 98, 96, 97 | midbtwn 27763 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) β (π΄πΌπ)) |
101 | 88 | ad4antr 731 |
. . . . . . . . . . . . 13
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β Β¬ π΄ β π·) |
102 | | nelne2 3043 |
. . . . . . . . . . . . 13
β’ (((π΄(midGβπΊ)π) β π· β§ Β¬ π΄ β π·) β (π΄(midGβπΊ)π) β π΄) |
103 | 87, 101, 102 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) β π΄) |
104 | 5, 6, 7, 95, 96, 99, 97, 100, 103 | tgbtwnne 27474 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π΄ β π) |
105 | 5, 7, 19, 95, 96, 97, 99, 104, 100 | btwnlng1 27603 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) β (π΄πΏπ)) |
106 | 5, 7, 19, 95, 96, 97, 104, 99, 103, 105 | tglineelsb2 27616 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄πΏπ) = (π΄πΏ(π΄(midGβπΊ)π))) |
107 | 78 | ad2antrr 725 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π· β ran πΏ) |
108 | 5, 7, 19, 95, 96, 97, 104 | tgelrnln 27614 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄πΏπ) β ran πΏ) |
109 | 104 | neneqd 2949 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β Β¬ π΄ = π) |
110 | | simprr 772 |
. . . . . . . . . . . . . 14
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) |
111 | 110 | orcomd 870 |
. . . . . . . . . . . . 13
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄ = π β¨ π·(βGβπΊ)(π΄πΏπ))) |
112 | 111 | ord 863 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (Β¬ π΄ = π β π·(βGβπΊ)(π΄πΏπ))) |
113 | 109, 112 | mpd 15 |
. . . . . . . . . . 11
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π·(βGβπΊ)(π΄πΏπ)) |
114 | 5, 6, 7, 19, 95, 107, 108, 113 | perpcom 27697 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄πΏπ)(βGβπΊ)π·) |
115 | 106, 114 | eqbrtrrd 5134 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄πΏ(π΄(midGβπΊ)π))(βGβπΊ)π·) |
116 | 86, 87, 92, 93, 94, 115 | rmoi2 3854 |
. . . . . . . 8
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π₯ = (π΄(midGβπΊ)π)) |
117 | 116 | eqcomd 2743 |
. . . . . . 7
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π΄(midGβπΊ)π) = π₯) |
118 | 80 | ad2antrr 725 |
. . . . . . . 8
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π₯ β π) |
119 | 5, 6, 7, 95, 98, 96, 97, 14, 118 | ismidb 27762 |
. . . . . . 7
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β (π = (((pInvGβπΊ)βπ₯)βπ΄) β (π΄(midGβπΊ)π) = π₯)) |
120 | 117, 119 | mpbird 257 |
. . . . . 6
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) β π = (((pInvGβπΊ)βπ₯)βπ΄)) |
121 | | simpr 486 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β π = (((pInvGβπΊ)βπ₯)βπ΄)) |
122 | 76 | ad2antrr 725 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β πΊ β TarskiG) |
123 | 10 | ad5antr 733 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β πΊDimTarskiGβ₯2) |
124 | 83 | ad2antrr 725 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β π΄ β π) |
125 | | simplr 768 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β π β π) |
126 | 80 | ad2antrr 725 |
. . . . . . . . . 10
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β π₯ β π) |
127 | 5, 6, 7, 122, 123, 124, 125, 14, 126 | ismidb 27762 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (π = (((pInvGβπΊ)βπ₯)βπ΄) β (π΄(midGβπΊ)π) = π₯)) |
128 | 121, 127 | mpbid 231 |
. . . . . . . 8
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (π΄(midGβπΊ)π) = π₯) |
129 | 79 | ad2antrr 725 |
. . . . . . . 8
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β π₯ β π·) |
130 | 128, 129 | eqeltrd 2838 |
. . . . . . 7
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (π΄(midGβπΊ)π) β π·) |
131 | 122 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β πΊ β TarskiG) |
132 | | simp-4r 783 |
. . . . . . . . . . . . 13
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β (π΄πΏπ₯)(βGβπΊ)π·) |
133 | 19, 131, 132 | perpln1 27694 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β (π΄πΏπ₯) β ran πΏ) |
134 | 78 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π· β ran πΏ) |
135 | 5, 6, 7, 19, 131, 133, 134, 132 | perpcom 27697 |
. . . . . . . . . . 11
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π·(βGβπΊ)(π΄πΏπ₯)) |
136 | 124 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π΄ β π) |
137 | 126 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π₯ β π) |
138 | 5, 7, 19, 131, 136, 137, 133 | tglnne 27612 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π΄ β π₯) |
139 | | simpllr 775 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π β π) |
140 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π΄ β π) |
141 | 140 | necomd 3000 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π β π΄) |
142 | 5, 6, 7, 19, 14, 131, 137, 81, 136 | mirbtwn 27642 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π₯ β ((((pInvGβπΊ)βπ₯)βπ΄)πΌπ΄)) |
143 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π = (((pInvGβπΊ)βπ₯)βπ΄)) |
144 | 143 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β (ππΌπ΄) = ((((pInvGβπΊ)βπ₯)βπ΄)πΌπ΄)) |
145 | 142, 144 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π₯ β (ππΌπ΄)) |
146 | 5, 7, 19, 131, 139, 136, 137, 141, 145 | btwnlng1 27603 |
. . . . . . . . . . . . 13
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π₯ β (ππΏπ΄)) |
147 | 5, 7, 19, 131, 136, 137, 139, 138, 146, 141 | lnrot1 27607 |
. . . . . . . . . . . 12
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π β (π΄πΏπ₯)) |
148 | 5, 7, 19, 131, 136, 137, 138, 139, 141, 147 | tglineelsb2 27616 |
. . . . . . . . . . 11
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β (π΄πΏπ₯) = (π΄πΏπ)) |
149 | 135, 148 | breqtrd 5136 |
. . . . . . . . . 10
β’
(((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β§ π΄ β π) β π·(βGβπΊ)(π΄πΏπ)) |
150 | 149 | ex 414 |
. . . . . . . . 9
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (π΄ β π β π·(βGβπΊ)(π΄πΏπ))) |
151 | 150 | necon1bd 2962 |
. . . . . . . 8
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (Β¬ π·(βGβπΊ)(π΄πΏπ) β π΄ = π)) |
152 | 151 | orrd 862 |
. . . . . . 7
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) |
153 | 130, 152 | jca 513 |
. . . . . 6
β’
((((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β§ π = (((pInvGβπΊ)βπ₯)βπ΄)) β ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
154 | 120, 153 | impbida 800 |
. . . . 5
β’
(((((π β§ Β¬
π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β§ π β π) β (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = (((pInvGβπΊ)βπ₯)βπ΄))) |
155 | 154 | ralrimiva 3144 |
. . . 4
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β βπ β π (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = (((pInvGβπΊ)βπ₯)βπ΄))) |
156 | | reu6i 3691 |
. . . 4
β’
(((((pInvGβπΊ)βπ₯)βπ΄) β π β§ βπ β π (((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π)) β π = (((pInvGβπΊ)βπ₯)βπ΄))) β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
157 | 84, 155, 156 | syl2anc 585 |
. . 3
β’ ((((π β§ Β¬ π΄ β π·) β§ π₯ β π·) β§ (π΄πΏπ₯)(βGβπΊ)π·) β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
158 | 5, 6, 7, 19, 75, 77, 82, 88 | footex 27705 |
. . 3
β’ ((π β§ Β¬ π΄ β π·) β βπ₯ β π· (π΄πΏπ₯)(βGβπΊ)π·) |
159 | 157, 158 | r19.29a 3160 |
. 2
β’ ((π β§ Β¬ π΄ β π·) β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |
160 | 74, 159 | pm2.61dan 812 |
1
β’ (π β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) |