Proof of Theorem hypcgrlem1
Step | Hyp | Ref
| Expression |
1 | | hypcgr.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | hypcgr.m |
. . 3
⊢ − =
(dist‘𝐺) |
3 | | hypcgr.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
4 | | hypcgr.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐺 ∈ TarskiG) |
6 | | hypcgr.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
7 | 6 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐶 ∈ 𝑃) |
8 | | hypcgr.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
9 | 8 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐴 ∈ 𝑃) |
10 | | hypcgr.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
11 | 10 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐹 ∈ 𝑃) |
12 | | hypcgr.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
13 | 12 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐷 ∈ 𝑃) |
14 | | eqid 2737 |
. . . . . . 7
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
15 | | eqid 2737 |
. . . . . . 7
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
16 | | hypcgr.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
17 | | hypcgr.1 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
18 | 1, 2, 3, 14, 15, 4, 8, 16, 6,
17 | ragcom 26789 |
. . . . . 6
⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉 ∈ (∟G‘𝐺)) |
19 | 1, 2, 3, 14, 15, 4, 6, 16, 8 | israg 26788 |
. . . . . 6
⊢ (𝜑 → (〈“𝐶𝐵𝐴”〉 ∈ (∟G‘𝐺) ↔ (𝐶 − 𝐴) = (𝐶 − (((pInvG‘𝐺)‘𝐵)‘𝐴)))) |
20 | 18, 19 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − (((pInvG‘𝐺)‘𝐵)‘𝐴))) |
21 | 20 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → (𝐶 − 𝐴) = (𝐶 − (((pInvG‘𝐺)‘𝐵)‘𝐴))) |
22 | | hypcgrlem1.a |
. . . . . . 7
⊢ (𝜑 → 𝐶 = 𝐹) |
23 | 22 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → 𝐹 = 𝐶) |
24 | 23 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐹 = 𝐶) |
25 | | hypcgr.h |
. . . . . . 7
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
26 | 1, 2, 3, 4, 25, 8,
12, 15, 16 | ismidb 26869 |
. . . . . 6
⊢ (𝜑 → (𝐷 = (((pInvG‘𝐺)‘𝐵)‘𝐴) ↔ (𝐴(midG‘𝐺)𝐷) = 𝐵)) |
27 | 26 | biimpar 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → 𝐷 = (((pInvG‘𝐺)‘𝐵)‘𝐴)) |
28 | 24, 27 | oveq12d 7231 |
. . . 4
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → (𝐹 − 𝐷) = (𝐶 − (((pInvG‘𝐺)‘𝐵)‘𝐴))) |
29 | 21, 28 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
30 | 1, 2, 3, 5, 7, 9, 11, 13, 29 | tgcgrcomlr 26571 |
. 2
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) = 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
31 | | simpr 488 |
. . . 4
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = 𝐷) → 𝐴 = 𝐷) |
32 | 22 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = 𝐷) → 𝐶 = 𝐹) |
33 | 31, 32 | oveq12d 7231 |
. . 3
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = 𝐷) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
34 | 17 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
35 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐺 ∈ TarskiG) |
36 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐴 ∈ 𝑃) |
37 | 16 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐵 ∈ 𝑃) |
38 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐶 ∈ 𝑃) |
39 | 1, 2, 3, 14, 15, 35, 36, 37, 38 | israg 26788 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − (((pInvG‘𝐺)‘𝐵)‘𝐶)))) |
40 | 34, 39 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − 𝐶) = (𝐴 − (((pInvG‘𝐺)‘𝐵)‘𝐶))) |
41 | 25 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐺DimTarskiG≥2) |
42 | | hypcgrlem1.s |
. . . . . . 7
⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
43 | 12 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐷 ∈ 𝑃) |
44 | 1, 2, 3, 35, 41, 36, 43 | midcl 26868 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ 𝑃) |
45 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) |
46 | 1, 3, 14, 35, 44, 37, 45 | tgelrnln 26721 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵) ∈ ran (LineG‘𝐺)) |
47 | | eqid 2737 |
. . . . . . 7
⊢
((pInvG‘𝐺)‘𝐵) = ((pInvG‘𝐺)‘𝐵) |
48 | | eqid 2737 |
. . . . . . . . 9
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
49 | 1, 2, 3, 14, 15, 35, 37, 47, 38 | mircl 26752 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (((pInvG‘𝐺)‘𝐵)‘𝐶) ∈ 𝑃) |
50 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐴 ≠ 𝐷) |
51 | 1, 2, 3, 35, 41, 36, 43 | midbtwn 26870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ (𝐴𝐼𝐷)) |
52 | 1, 14, 3, 35, 36, 44, 43, 51 | btwncolg3 26648 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷 ∈ (𝐴(LineG‘𝐺)(𝐴(midG‘𝐺)𝐷)) ∨ 𝐴 = (𝐴(midG‘𝐺)𝐷))) |
53 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 = 𝐷) |
54 | | hypcgrlem2.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = 𝐸) |
55 | 53, 54, 22 | s3eqd 14429 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝐷𝐵𝐶”〉 = 〈“𝐷𝐸𝐹”〉) |
56 | 55 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“𝐷𝐵𝐶”〉 = 〈“𝐷𝐸𝐹”〉) |
57 | | hypcgr.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
58 | 57 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
59 | 56, 58 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“𝐷𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
60 | 1, 2, 3, 14, 15, 35, 43, 37, 38 | israg 26788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (〈“𝐷𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐷 − 𝐶) = (𝐷 − (((pInvG‘𝐺)‘𝐵)‘𝐶)))) |
61 | 59, 60 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷 − 𝐶) = (𝐷 − (((pInvG‘𝐺)‘𝐵)‘𝐶))) |
62 | 1, 14, 3, 35, 36, 43, 44, 48, 38, 49, 2, 50, 52, 40, 61 | lncgr 26660 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → ((𝐴(midG‘𝐺)𝐷) − 𝐶) = ((𝐴(midG‘𝐺)𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐶))) |
63 | 1, 2, 3, 14, 15, 35, 44, 37, 38 | israg 26788 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (〈“(𝐴(midG‘𝐺)𝐷)𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ ((𝐴(midG‘𝐺)𝐷) − 𝐶) = ((𝐴(midG‘𝐺)𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐶)))) |
64 | 62, 63 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“(𝐴(midG‘𝐺)𝐷)𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
65 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx1 26724 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
66 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx2 26725 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐵 ∈ ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
67 | 1, 2, 3, 35, 41, 42, 14, 46, 44, 47, 64, 65, 66, 38, 45 | lmimid 26885 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝑆‘𝐶) = (((pInvG‘𝐺)‘𝐵)‘𝐶)) |
68 | 67 | oveq2d 7229 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − (𝑆‘𝐶)) = (𝐴 − (((pInvG‘𝐺)‘𝐵)‘𝐶))) |
69 | 40, 68 | eqtr4d 2780 |
. . . 4
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − 𝐶) = (𝐴 − (𝑆‘𝐶))) |
70 | 1, 2, 3, 35, 41, 43, 36 | midcom 26873 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷(midG‘𝐺)𝐴) = (𝐴(midG‘𝐺)𝐷)) |
71 | 70, 65 | eqeltrd 2838 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷(midG‘𝐺)𝐴) ∈ ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
72 | 50 | necomd 2996 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐷 ≠ 𝐴) |
73 | 1, 3, 14, 35, 43, 36, 72 | tgelrnln 26721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷(LineG‘𝐺)𝐴) ∈ ran (LineG‘𝐺)) |
74 | 1, 2, 3, 35, 36, 44, 43, 51 | tgbtwncom 26579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ (𝐷𝐼𝐴)) |
75 | 1, 3, 14, 35, 43, 36, 44, 72, 74 | btwnlng1 26710 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ (𝐷(LineG‘𝐺)𝐴)) |
76 | 65, 75 | elind 4108 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) ∈ (((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵) ∩ (𝐷(LineG‘𝐺)𝐴))) |
77 | 1, 3, 14, 35, 43, 36, 72 | tglinerflx2 26725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐴 ∈ (𝐷(LineG‘𝐺)𝐴)) |
78 | 45 | necomd 2996 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐵 ≠ (𝐴(midG‘𝐺)𝐷)) |
79 | 4 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG) |
80 | 8 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃) |
81 | 12 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃) |
82 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐺DimTarskiG≥2) |
83 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐴 = (𝐴(midG‘𝐺)𝐷)) |
84 | 83 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → (𝐴(midG‘𝐺)𝐷) = 𝐴) |
85 | 1, 2, 3, 79, 82, 80, 81, 84 | midcgr 26871 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → (𝐴 − 𝐴) = (𝐴 − 𝐷)) |
86 | 85 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → (𝐴 − 𝐷) = (𝐴 − 𝐴)) |
87 | 1, 2, 3, 79, 80, 81, 80, 86 | axtgcgrid 26554 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 = (𝐴(midG‘𝐺)𝐷)) → 𝐴 = 𝐷) |
88 | 87 | ex 416 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) → (𝐴 = (𝐴(midG‘𝐺)𝐷) → 𝐴 = 𝐷)) |
89 | 88 | necon3d 2961 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) → (𝐴 ≠ 𝐷 → 𝐴 ≠ (𝐴(midG‘𝐺)𝐷))) |
90 | 89 | imp 410 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐴 ≠ (𝐴(midG‘𝐺)𝐷)) |
91 | | hypcgr.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
92 | | hypcgr.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
93 | 1, 2, 3, 4, 8, 16,
12, 91, 92 | tgcgrcomlr 26571 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
94 | 54 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐷) = (𝐸 − 𝐷)) |
95 | 93, 94 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐵 − 𝐷)) |
96 | 95 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐵 − 𝐴) = (𝐵 − 𝐷)) |
97 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴(midG‘𝐺)𝐷) = (𝐴(midG‘𝐺)𝐷)) |
98 | 1, 2, 3, 35, 41, 36, 43, 15, 44 | ismidb 26869 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐷))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐷) = (𝐴(midG‘𝐺)𝐷))) |
99 | 97, 98 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐷 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐷))‘𝐴)) |
100 | 99 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐵 − 𝐷) = (𝐵 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐷))‘𝐴))) |
101 | 96, 100 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐵 − 𝐴) = (𝐵 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐷))‘𝐴))) |
102 | 1, 2, 3, 14, 15, 35, 37, 44, 36 | israg 26788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (〈“𝐵(𝐴(midG‘𝐺)𝐷)𝐴”〉 ∈ (∟G‘𝐺) ↔ (𝐵 − 𝐴) = (𝐵 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐷))‘𝐴)))) |
103 | 101, 102 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 〈“𝐵(𝐴(midG‘𝐺)𝐷)𝐴”〉 ∈ (∟G‘𝐺)) |
104 | 1, 2, 3, 14, 35, 46, 73, 76, 66, 77, 78, 90, 103 | ragperp 26808 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐷(LineG‘𝐺)𝐴)) |
105 | 104 | orcd 873 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐷(LineG‘𝐺)𝐴) ∨ 𝐷 = 𝐴)) |
106 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 36 | islmib 26878 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 = (𝑆‘𝐷) ↔ ((𝐷(midG‘𝐺)𝐴) ∈ ((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵) ∧ (((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐷(LineG‘𝐺)𝐴) ∨ 𝐷 = 𝐴)))) |
107 | 71, 105, 106 | mpbir2and 713 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → 𝐴 = (𝑆‘𝐷)) |
108 | 107 | oveq1d 7228 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − (𝑆‘𝐶)) = ((𝑆‘𝐷) − (𝑆‘𝐶))) |
109 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 38 | lmiiso 26888 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → ((𝑆‘𝐷) − (𝑆‘𝐶)) = (𝐷 − 𝐶)) |
110 | 22 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → (𝐷 − 𝐶) = (𝐷 − 𝐹)) |
111 | 110 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐷 − 𝐶) = (𝐷 − 𝐹)) |
112 | 108, 109,
111 | 3eqtrd 2781 |
. . . 4
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − (𝑆‘𝐶)) = (𝐷 − 𝐹)) |
113 | 69, 112 | eqtrd 2777 |
. . 3
⊢ (((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) ∧ 𝐴 ≠ 𝐷) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
114 | 33, 113 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐷) ≠ 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
115 | 30, 114 | pm2.61dane 3029 |
1
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |