Proof of Theorem hypcgrlem2
| Step | Hyp | Ref
| Expression |
| 1 | | hypcgr.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | hypcgr.m |
. . . 4
⊢ − =
(dist‘𝐺) |
| 3 | | hypcgr.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | hypcgr.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐺 ∈ TarskiG) |
| 6 | | hypcgr.h |
. . . . 5
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐺DimTarskiG≥2) |
| 8 | | hypcgr.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐴 ∈ 𝑃) |
| 10 | | hypcgr.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐵 ∈ 𝑃) |
| 12 | | hypcgr.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐶 ∈ 𝑃) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
| 15 | | eqid 2737 |
. . . . 5
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
| 16 | | eqid 2737 |
. . . . 5
⊢
((pInvG‘𝐺)‘𝐵) = ((pInvG‘𝐺)‘𝐵) |
| 17 | | hypcgr.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 18 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐷 ∈ 𝑃) |
| 19 | 1, 2, 3, 14, 15, 5, 11, 16, 18 | mircl 28669 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (((pInvG‘𝐺)‘𝐵)‘𝐷) ∈ 𝑃) |
| 20 | | hypcgr.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 21 | 20 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐸 ∈ 𝑃) |
| 22 | | hypcgr.1 |
. . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 24 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (((pInvG‘𝐺)‘𝐵)‘𝐷) = (((pInvG‘𝐺)‘𝐵)‘𝐷)) |
| 25 | | hypcgrlem2.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = 𝐸) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐵 = 𝐸) |
| 27 | 1, 2, 3, 14, 15, 5, 11, 16, 21 | mirinv 28674 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐸) = 𝐸 ↔ 𝐵 = 𝐸)) |
| 28 | 26, 27 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (((pInvG‘𝐺)‘𝐵)‘𝐸) = 𝐸) |
| 29 | 28 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐸 = (((pInvG‘𝐺)‘𝐵)‘𝐸)) |
| 30 | | hypcgr.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐹 ∈ 𝑃) |
| 32 | 1, 2, 3, 5, 7, 13,
31 | midcom 28790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶(midG‘𝐺)𝐹) = (𝐹(midG‘𝐺)𝐶)) |
| 33 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶(midG‘𝐺)𝐹) = 𝐵) |
| 34 | 32, 33 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐹(midG‘𝐺)𝐶) = 𝐵) |
| 35 | 1, 2, 3, 5, 7, 31,
13, 15, 11 | ismidb 28786 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶 = (((pInvG‘𝐺)‘𝐵)‘𝐹) ↔ (𝐹(midG‘𝐺)𝐶) = 𝐵)) |
| 36 | 34, 35 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐶 = (((pInvG‘𝐺)‘𝐵)‘𝐹)) |
| 37 | 24, 29, 36 | s3eqd 14903 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“(((pInvG‘𝐺)‘𝐵)‘𝐷)𝐸𝐶”〉 =
〈“(((pInvG‘𝐺)‘𝐵)‘𝐷)(((pInvG‘𝐺)‘𝐵)‘𝐸)(((pInvG‘𝐺)‘𝐵)‘𝐹)”〉) |
| 38 | | hypcgr.2 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 39 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 40 | 1, 2, 3, 14, 15, 5, 18, 21, 31, 39, 16, 11 | mirrag 28709 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“(((pInvG‘𝐺)‘𝐵)‘𝐷)(((pInvG‘𝐺)‘𝐵)‘𝐸)(((pInvG‘𝐺)‘𝐵)‘𝐹)”〉 ∈ (∟G‘𝐺)) |
| 41 | 37, 40 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“(((pInvG‘𝐺)‘𝐵)‘𝐷)𝐸𝐶”〉 ∈ (∟G‘𝐺)) |
| 42 | | hypcgr.3 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 43 | 42 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 44 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 21 | miriso 28678 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐸)) = (𝐷 − 𝐸)) |
| 45 | 28 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐸)) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐸)) |
| 46 | 43, 44, 45 | 3eqtr2d 2783 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐵) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐸)) |
| 47 | 26 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐶)) |
| 48 | | eqid 2737 |
. . . 4
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(((pInvG‘𝐺)‘𝐵)‘𝐷))(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(((pInvG‘𝐺)‘𝐵)‘𝐷))(LineG‘𝐺)𝐵)) |
| 49 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐶 = 𝐶) |
| 50 | 1, 2, 3, 5, 7, 9, 11, 13, 19, 21, 13, 23, 41, 46, 47, 26, 48, 49 | hypcgrlem1 28807 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐶) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐶)) |
| 51 | 36 | oveq2d 7447 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐶) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐹))) |
| 52 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 31 | miriso 28678 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐹)) = (𝐷 − 𝐹)) |
| 53 | 50, 51, 52 | 3eqtrd 2781 |
. 2
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 54 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐺 ∈ TarskiG) |
| 55 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐺DimTarskiG≥2) |
| 56 | 8 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐴 ∈ 𝑃) |
| 57 | 10 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐵 ∈ 𝑃) |
| 58 | 12 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐶 ∈ 𝑃) |
| 59 | 17 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐷 ∈ 𝑃) |
| 60 | 20 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐸 ∈ 𝑃) |
| 61 | 30 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐹 ∈ 𝑃) |
| 62 | 22 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 63 | 38 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 64 | 42 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 65 | | hypcgr.4 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 66 | 65 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 67 | 25 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐵 = 𝐸) |
| 68 | | eqid 2737 |
. . . 4
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
| 69 | | simpr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐶 = 𝐹) |
| 70 | 1, 2, 3, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 66, 67, 68, 69 | hypcgrlem1 28807 |
. . 3
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 71 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐺 ∈ TarskiG) |
| 72 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐺DimTarskiG≥2) |
| 73 | 8 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐴 ∈ 𝑃) |
| 74 | 10 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ∈ 𝑃) |
| 75 | 12 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ∈ 𝑃) |
| 76 | | hypcgrlem2.s |
. . . . . 6
⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
| 77 | 30 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 ∈ 𝑃) |
| 78 | 1, 2, 3, 71, 72, 75, 77 | midcl 28785 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ 𝑃) |
| 79 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) |
| 80 | 1, 3, 14, 71, 78, 74, 79 | tgelrnln 28638 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∈ ran (LineG‘𝐺)) |
| 81 | 17 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐷 ∈ 𝑃) |
| 82 | 1, 2, 3, 71, 72, 76, 14, 80, 81 | lmicl 28794 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐷) ∈ 𝑃) |
| 83 | 20 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐸 ∈ 𝑃) |
| 84 | 1, 2, 3, 71, 72, 76, 14, 80, 83 | lmicl 28794 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐸) ∈ 𝑃) |
| 85 | 1, 2, 3, 71, 72, 76, 14, 80, 77 | lmicl 28794 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐹) ∈ 𝑃) |
| 86 | 22 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
| 87 | 1, 2, 3, 71, 72, 76, 14, 80 | lmimot 28806 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝑆 ∈ (𝐺Ismt𝐺)) |
| 88 | 38 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
| 89 | 1, 2, 3, 14, 15, 71, 81, 83, 77, 87, 88 | motrag 28716 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“(𝑆‘𝐷)(𝑆‘𝐸)(𝑆‘𝐹)”〉 ∈ (∟G‘𝐺)) |
| 90 | 42 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 91 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 83 | lmiiso 28805 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐷) − (𝑆‘𝐸)) = (𝐷 − 𝐸)) |
| 92 | 90, 91 | eqtr4d 2780 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐵) = ((𝑆‘𝐷) − (𝑆‘𝐸))) |
| 93 | 65 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 94 | 1, 2, 3, 71, 72, 76, 14, 80, 83, 77 | lmiiso 28805 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐸) − (𝑆‘𝐹)) = (𝐸 − 𝐹)) |
| 95 | 93, 94 | eqtr4d 2780 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = ((𝑆‘𝐸) − (𝑆‘𝐹))) |
| 96 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx2 28642 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
| 97 | 1, 2, 3, 71, 72, 76, 14, 80, 74, 96 | lmicinv 28801 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐵) = 𝐵) |
| 98 | 25 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 = 𝐸) |
| 99 | 98 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐵) = (𝑆‘𝐸)) |
| 100 | 97, 99 | eqtr3d 2779 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 = (𝑆‘𝐸)) |
| 101 | | eqid 2737 |
. . . . 5
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑆‘𝐷))(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑆‘𝐷))(LineG‘𝐺)𝐵)) |
| 102 | 1, 2, 3, 71, 72, 75, 77 | midcom 28790 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) = (𝐹(midG‘𝐺)𝐶)) |
| 103 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx1 28641 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
| 104 | 102, 103 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹(midG‘𝐺)𝐶) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
| 105 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ≠ 𝐹) |
| 106 | 105 | necomd 2996 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 ≠ 𝐶) |
| 107 | 1, 3, 14, 71, 77, 75, 106 | tgelrnln 28638 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹(LineG‘𝐺)𝐶) ∈ ran (LineG‘𝐺)) |
| 108 | 1, 2, 3, 71, 72, 75, 77 | midbtwn 28787 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐶𝐼𝐹)) |
| 109 | 1, 2, 3, 71, 75, 78, 77, 108 | tgbtwncom 28496 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐹𝐼𝐶)) |
| 110 | 1, 3, 14, 71, 77, 75, 78, 106, 109 | btwnlng1 28627 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐹(LineG‘𝐺)𝐶)) |
| 111 | 103, 110 | elind 4200 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∩ (𝐹(LineG‘𝐺)𝐶))) |
| 112 | 1, 3, 14, 71, 77, 75, 106 | tglinerflx2 28642 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ∈ (𝐹(LineG‘𝐺)𝐶)) |
| 113 | 79 | necomd 2996 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ≠ (𝐶(midG‘𝐺)𝐹)) |
| 114 | 4 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐺 ∈ TarskiG) |
| 115 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 ∈ 𝑃) |
| 116 | 30 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐹 ∈ 𝑃) |
| 117 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐺DimTarskiG≥2) |
| 118 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 = (𝐶(midG‘𝐺)𝐹)) |
| 119 | 118 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶(midG‘𝐺)𝐹) = 𝐶) |
| 120 | 1, 2, 3, 114, 117, 115, 116, 119 | midcgr 28788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶 − 𝐶) = (𝐶 − 𝐹)) |
| 121 | 120 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶 − 𝐹) = (𝐶 − 𝐶)) |
| 122 | 1, 2, 3, 114, 115, 116, 115, 121 | axtgcgrid 28471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 = 𝐹) |
| 123 | 122 | ex 412 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐶 = (𝐶(midG‘𝐺)𝐹) → 𝐶 = 𝐹)) |
| 124 | 123 | necon3d 2961 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐶 ≠ 𝐹 → 𝐶 ≠ (𝐶(midG‘𝐺)𝐹))) |
| 125 | 124 | imp 406 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ≠ (𝐶(midG‘𝐺)𝐹)) |
| 126 | 98 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐸 = 𝐵) |
| 127 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) = (𝐶(midG‘𝐺)𝐹)) |
| 128 | 1, 2, 3, 71, 72, 75, 77, 15, 78 | ismidb 28786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹 = (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶) ↔ (𝐶(midG‘𝐺)𝐹) = (𝐶(midG‘𝐺)𝐹))) |
| 129 | 127, 128 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 = (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶)) |
| 130 | 126, 129 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐸 − 𝐹) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶))) |
| 131 | 93, 130 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶))) |
| 132 | 1, 2, 3, 14, 15, 71, 74, 78, 75 | israg 28705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (〈“𝐵(𝐶(midG‘𝐺)𝐹)𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐵 − 𝐶) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶)))) |
| 133 | 131, 132 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐵(𝐶(midG‘𝐺)𝐹)𝐶”〉 ∈ (∟G‘𝐺)) |
| 134 | 1, 2, 3, 14, 71, 80, 107, 111, 96, 112, 113, 125, 133 | ragperp 28725 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶)) |
| 135 | 134 | orcd 874 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶) ∨ 𝐹 = 𝐶)) |
| 136 | 1, 2, 3, 71, 72, 76, 14, 80, 77, 75 | islmib 28795 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶 = (𝑆‘𝐹) ↔ ((𝐹(midG‘𝐺)𝐶) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∧ (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶) ∨ 𝐹 = 𝐶)))) |
| 137 | 104, 135,
136 | mpbir2and 713 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 = (𝑆‘𝐹)) |
| 138 | 1, 2, 3, 71, 72, 73, 74, 75, 82, 84, 85, 86, 89, 92, 95, 100, 101, 137 | hypcgrlem1 28807 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐶) = ((𝑆‘𝐷) − (𝑆‘𝐹))) |
| 139 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 77 | lmiiso 28805 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐷) − (𝑆‘𝐹)) = (𝐷 − 𝐹)) |
| 140 | 138, 139 | eqtrd 2777 |
. . 3
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 141 | 70, 140 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 142 | 53, 141 | pm2.61dane 3029 |
1
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |