Proof of Theorem lmimid
Step | Hyp | Ref
| Expression |
1 | | lmimid.s |
. . . . . . 7
⊢ 𝑆 = ((pInvG‘𝐺)‘𝐵) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑆 = ((pInvG‘𝐺)‘𝐵)) |
3 | 2 | fveq1d 6770 |
. . . . 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 2739 |
. . . . . . 7
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
12 | | lmif.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
13 | | lmimid.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
14 | 4, 10, 6, 7, 12, 13 | tglnpt 26891 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
15 | 4, 5, 6, 10, 11, 7, 14, 1, 9 | mircl 27003 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑃) |
16 | 4, 5, 6, 7, 8, 9, 15, 11, 14 | ismidb 27120 |
. . . . 5
⊢ (𝜑 → ((𝑆‘𝐶) = (((pInvG‘𝐺)‘𝐵)‘𝐶) ↔ (𝐶(midG‘𝐺)(𝑆‘𝐶)) = 𝐵)) |
17 | 3, 16 | mpbid 231 |
. . . 4
⊢ (𝜑 → (𝐶(midG‘𝐺)(𝑆‘𝐶)) = 𝐵) |
18 | 17, 13 | eqeltrd 2840 |
. . 3
⊢ (𝜑 → (𝐶(midG‘𝐺)(𝑆‘𝐶)) ∈ 𝐷) |
19 | | df-ne 2945 |
. . . . . 6
⊢ (𝐶 ≠ (𝑆‘𝐶) ↔ ¬ 𝐶 = (𝑆‘𝐶)) |
20 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐺 ∈ TarskiG) |
21 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐷 ∈ ran 𝐿) |
22 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐶 ∈ 𝑃) |
23 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → (𝑆‘𝐶) ∈ 𝑃) |
24 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐶 ≠ (𝑆‘𝐶)) |
25 | 4, 6, 10, 20, 22, 23, 24 | tgelrnln 26972 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → (𝐶𝐿(𝑆‘𝐶)) ∈ ran 𝐿) |
26 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐵 ∈ 𝐷) |
27 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐵 ∈ 𝑃) |
28 | 4, 5, 6, 7, 8, 9, 15 | midbtwn 27121 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶(midG‘𝐺)(𝑆‘𝐶)) ∈ (𝐶𝐼(𝑆‘𝐶))) |
29 | 17, 28 | eqeltrrd 2841 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼(𝑆‘𝐶))) |
30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐵 ∈ (𝐶𝐼(𝑆‘𝐶))) |
31 | 4, 6, 10, 20, 22, 23, 27, 24, 30 | btwnlng1 26961 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐵 ∈ (𝐶𝐿(𝑆‘𝐶))) |
32 | 26, 31 | elind 4132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐵 ∈ (𝐷 ∩ (𝐶𝐿(𝑆‘𝐶)))) |
33 | | lmimid.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐴 ∈ 𝐷) |
35 | 4, 6, 10, 20, 22, 23, 24 | tglinerflx1 26975 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐶 ∈ (𝐶𝐿(𝑆‘𝐶))) |
36 | | lmimid.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐴 ≠ 𝐵) |
38 | 4, 5, 6, 10, 11, 7, 14, 1, 9 | mirinv 27008 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑆‘𝐶) = 𝐶 ↔ 𝐵 = 𝐶)) |
39 | | eqcom 2746 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵) |
40 | 38, 39 | bitrdi 286 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆‘𝐶) = 𝐶 ↔ 𝐶 = 𝐵)) |
41 | 40 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → (𝑆‘𝐶) = 𝐶) |
42 | 41 | eqcomd 2745 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → 𝐶 = (𝑆‘𝐶)) |
43 | 42 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 = 𝐵 → 𝐶 = (𝑆‘𝐶))) |
44 | 43 | necon3d 2965 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ≠ (𝑆‘𝐶) → 𝐶 ≠ 𝐵)) |
45 | 44 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐶 ≠ 𝐵) |
46 | | lmimid.r |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
48 | 4, 5, 6, 10, 20, 21, 25, 32, 34, 35, 37, 45, 47 | ragperp 27059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ≠ (𝑆‘𝐶)) → 𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶))) |
49 | 48 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝐶 ≠ (𝑆‘𝐶) → 𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶)))) |
50 | 19, 49 | syl5bir 242 |
. . . . 5
⊢ (𝜑 → (¬ 𝐶 = (𝑆‘𝐶) → 𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶)))) |
51 | 50 | orrd 859 |
. . . 4
⊢ (𝜑 → (𝐶 = (𝑆‘𝐶) ∨ 𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶)))) |
52 | 51 | orcomd 867 |
. . 3
⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶)) ∨ 𝐶 = (𝑆‘𝐶))) |
53 | | lmif.m |
. . . 4
⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) |
54 | 4, 5, 6, 7, 8, 53,
10, 12, 9, 15 | islmib 27129 |
. . 3
⊢ (𝜑 → ((𝑆‘𝐶) = (𝑀‘𝐶) ↔ ((𝐶(midG‘𝐺)(𝑆‘𝐶)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐶𝐿(𝑆‘𝐶)) ∨ 𝐶 = (𝑆‘𝐶))))) |
55 | 18, 52, 54 | mpbir2and 709 |
. 2
⊢ (𝜑 → (𝑆‘𝐶) = (𝑀‘𝐶)) |
56 | 55 | eqcomd 2745 |
1
⊢ (𝜑 → (𝑀‘𝐶) = (𝑆‘𝐶)) |