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