Proof of Theorem colmid
Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
2 | 1 | olcd 408 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
3 | | mirval.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
4 | | mirval.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
5 | | mirval.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
6 | | mirval.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
7 | | mirval.s |
. . . . 5
⊢ 𝑆 = (pInvG‘𝐺) |
8 | | mirval.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
9 | 8 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
10 | | colmid.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
11 | 10 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ 𝑃) |
12 | | colmid.m |
. . . . 5
⊢ 𝑀 = (𝑆‘𝑋) |
13 | | colmid.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
14 | 13 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
15 | | colmid.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
16 | 15 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃) |
17 | | colmid.d |
. . . . . . 7
⊢ (𝜑 → (𝑋 − 𝐴) = (𝑋 − 𝐵)) |
18 | 17 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝑋 − 𝐴) = (𝑋 − 𝐵)) |
19 | 18 | eqcomd 2628 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝑋 − 𝐵) = (𝑋 − 𝐴)) |
20 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ (𝐴𝐼𝐵)) |
21 | 3, 4, 5, 9, 14, 11, 16, 20 | tgbtwncom 25383 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝑋 ∈ (𝐵𝐼𝐴)) |
22 | 3, 4, 5, 6, 7, 9, 11, 12, 14, 16, 19, 21 | ismir 25554 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → 𝐵 = (𝑀‘𝐴)) |
23 | 22 | orcd 407 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ (𝐴𝐼𝐵)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
24 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐺 ∈ TarskiG) |
25 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐵 ∈ 𝑃) |
26 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ 𝑃) |
27 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝑋 ∈ 𝑃) |
28 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝑋𝐼𝐵)) |
29 | 3, 4, 5, 24, 27, 26, 25, 28 | tgbtwncom 25383 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝑋)) |
30 | 3, 4, 5, 24, 26, 27 | tgbtwntriv1 25386 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 ∈ (𝐴𝐼𝑋)) |
31 | 3, 4, 5, 8, 10, 13, 10, 15, 17 | tgcgrcomlr 25375 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
32 | 31 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
33 | 32 | eqcomd 2628 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 − 𝑋) = (𝐴 − 𝑋)) |
34 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐴 − 𝑋) = (𝐴 − 𝑋)) |
35 | 3, 4, 5, 24, 25, 26, 27, 26, 26, 27, 29, 30, 33, 34 | tgcgrsub 25404 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 − 𝐴) = (𝐴 − 𝐴)) |
36 | 3, 4, 5, 24, 25, 26, 26, 35 | axtgcgrid 25362 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐵 = 𝐴) |
37 | 36 | eqcomd 2628 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 = 𝐵) |
38 | 37 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → 𝐴 = 𝐵) |
39 | 38 | olcd 408 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ (𝑋𝐼𝐵)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
40 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐺 ∈ TarskiG) |
41 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 ∈ 𝑃) |
42 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ 𝑃) |
43 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝑋 ∈ 𝑃) |
44 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ (𝐴𝐼𝑋)) |
45 | 3, 4, 5, 40, 42, 43 | tgbtwntriv1 25386 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐵 ∈ (𝐵𝐼𝑋)) |
46 | 31 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐴 − 𝑋) = (𝐵 − 𝑋)) |
47 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐵 − 𝑋) = (𝐵 − 𝑋)) |
48 | 3, 4, 5, 40, 41, 42, 43, 42, 42, 43, 44, 45, 46, 47 | tgcgrsub 25404 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐴 − 𝐵) = (𝐵 − 𝐵)) |
49 | 3, 4, 5, 40, 41, 42, 42, 48 | axtgcgrid 25362 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 = 𝐵) |
50 | 49 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → 𝐴 = 𝐵) |
51 | 50 | olcd 408 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐵 ∈ (𝐴𝐼𝑋)) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
52 | | df-ne 2795 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
53 | | colmid.c |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
54 | 53 | orcomd 403 |
. . . . . 6
⊢ (𝜑 → (𝐴 = 𝐵 ∨ 𝑋 ∈ (𝐴𝐿𝐵))) |
55 | 54 | orcanai 952 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = 𝐵) → 𝑋 ∈ (𝐴𝐿𝐵)) |
56 | 52, 55 | sylan2b 492 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝑋 ∈ (𝐴𝐿𝐵)) |
57 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
58 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
59 | 15 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
60 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
61 | 10 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝑋 ∈ 𝑃) |
62 | 3, 6, 5, 57, 58, 59, 60, 61 | tgellng 25448 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑋 ∈ (𝐴𝐿𝐵) ↔ (𝑋 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝑋𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝑋)))) |
63 | 56, 62 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑋 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝑋𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝑋))) |
64 | 23, 39, 51, 63 | mpjao3dan 1395 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |
65 | 2, 64 | pm2.61dane 2881 |
1
⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) |