Proof of Theorem krippen
Step | Hyp | Ref
| Expression |
1 | | mirval.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | mirval.d |
. . 3
⊢ − =
(dist‘𝐺) |
3 | | mirval.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
4 | | mirval.l |
. . 3
⊢ 𝐿 = (LineG‘𝐺) |
5 | | mirval.s |
. . 3
⊢ 𝑆 = (pInvG‘𝐺) |
6 | | mirval.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 6 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐺 ∈ TarskiG) |
8 | | krippen.m |
. . 3
⊢ 𝑀 = (𝑆‘𝑋) |
9 | | krippen.n |
. . 3
⊢ 𝑁 = (𝑆‘𝑌) |
10 | | krippen.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
11 | 10 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐴 ∈ 𝑃) |
12 | | krippen.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
13 | 12 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐵 ∈ 𝑃) |
14 | | krippen.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
15 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐶 ∈ 𝑃) |
16 | | krippen.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
17 | 16 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐸 ∈ 𝑃) |
18 | | krippen.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
19 | 18 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐹 ∈ 𝑃) |
20 | | krippen.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
21 | 20 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝑋 ∈ 𝑃) |
22 | | krippen.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
23 | 22 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝑌 ∈ 𝑃) |
24 | | krippen.1 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐸)) |
25 | 24 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐶 ∈ (𝐴𝐼𝐸)) |
26 | | krippen.2 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐹)) |
27 | 26 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐶 ∈ (𝐵𝐼𝐹)) |
28 | | krippen.3 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) |
29 | 28 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → (𝐶 − 𝐴) = (𝐶 − 𝐵)) |
30 | | krippen.4 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐸) = (𝐶 − 𝐹)) |
31 | 30 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → (𝐶 − 𝐸) = (𝐶 − 𝐹)) |
32 | | krippen.5 |
. . . 4
⊢ (𝜑 → 𝐵 = (𝑀‘𝐴)) |
33 | 32 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐵 = (𝑀‘𝐴)) |
34 | | krippen.6 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑁‘𝐸)) |
35 | 34 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐹 = (𝑁‘𝐸)) |
36 | | eqid 2622 |
. . 3
⊢
(≤G‘𝐺) =
(≤G‘𝐺) |
37 | | simpr 477 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) |
38 | 1, 2, 3, 4, 5, 7, 8, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 36, 37 | krippenlem 25585 |
. 2
⊢ ((𝜑 ∧ (𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸)) → 𝐶 ∈ (𝑋𝐼𝑌)) |
39 | 6 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐺 ∈ TarskiG) |
40 | 22 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝑌 ∈ 𝑃) |
41 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ 𝑃) |
42 | 20 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝑋 ∈ 𝑃) |
43 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐸 ∈ 𝑃) |
44 | 18 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐹 ∈ 𝑃) |
45 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐴 ∈ 𝑃) |
46 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐵 ∈ 𝑃) |
47 | 24 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝐴𝐼𝐸)) |
48 | 1, 2, 3, 39, 45, 41, 43, 47 | tgbtwncom 25383 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝐸𝐼𝐴)) |
49 | 26 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝐵𝐼𝐹)) |
50 | 1, 2, 3, 39, 46, 41, 44, 49 | tgbtwncom 25383 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝐹𝐼𝐵)) |
51 | 30 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → (𝐶 − 𝐸) = (𝐶 − 𝐹)) |
52 | 28 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → (𝐶 − 𝐴) = (𝐶 − 𝐵)) |
53 | 34 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐹 = (𝑁‘𝐸)) |
54 | 32 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐵 = (𝑀‘𝐴)) |
55 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) |
56 | 1, 2, 3, 4, 5, 39,
9, 8, 43, 44, 41, 45, 46, 40, 42, 48, 50, 51, 52, 53, 54, 36, 55 | krippenlem 25585 |
. . 3
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝑌𝐼𝑋)) |
57 | 1, 2, 3, 39, 40, 41, 42, 56 | tgbtwncom 25383 |
. 2
⊢ ((𝜑 ∧ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴)) → 𝐶 ∈ (𝑋𝐼𝑌)) |
58 | 1, 2, 3, 36, 6, 14, 10, 14, 16 | legtrid 25486 |
. 2
⊢ (𝜑 → ((𝐶 − 𝐴)(≤G‘𝐺)(𝐶 − 𝐸) ∨ (𝐶 − 𝐸)(≤G‘𝐺)(𝐶 − 𝐴))) |
59 | 38, 57, 58 | mpjaodan 827 |
1
⊢ (𝜑 → 𝐶 ∈ (𝑋𝐼𝑌)) |