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 2610 |
. . . . 5
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
15 | | eqid 2610 |
. . . . 5
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
16 | | eqid 2610 |
. . . . 5
⊢
((pInvG‘𝐺)‘𝐵) = ((pInvG‘𝐺)‘𝐵) |
17 | | hypcgr.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
18 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐷 ∈ 𝑃) |
19 | 1, 2, 3, 14, 15, 5, 11, 16, 18 | mircl 25356 |
. . . 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 2611 |
. . . . . 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 25361 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐸) = 𝐸 ↔ 𝐵 = 𝐸)) |
28 | 26, 27 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (((pInvG‘𝐺)‘𝐵)‘𝐸) = 𝐸) |
29 | 28 | eqcomd 2616 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐸 = (((pInvG‘𝐺)‘𝐵)‘𝐸)) |
30 | | hypcgr.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐹 ∈ 𝑃) |
32 | 1, 2, 3, 5, 7, 13,
31 | midcom 25474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶(midG‘𝐺)𝐹) = (𝐹(midG‘𝐺)𝐶)) |
33 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶(midG‘𝐺)𝐹) = 𝐵) |
34 | 32, 33 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐹(midG‘𝐺)𝐶) = 𝐵) |
35 | 1, 2, 3, 5, 7, 31,
13, 15, 11 | ismidb 25470 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐶 = (((pInvG‘𝐺)‘𝐵)‘𝐹) ↔ (𝐹(midG‘𝐺)𝐶) = 𝐵)) |
36 | 34, 35 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐶 = (((pInvG‘𝐺)‘𝐵)‘𝐹)) |
37 | 24, 29, 36 | s3eqd 13460 |
. . . . 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 25396 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 〈“(((pInvG‘𝐺)‘𝐵)‘𝐷)(((pInvG‘𝐺)‘𝐵)‘𝐸)(((pInvG‘𝐺)‘𝐵)‘𝐹)”〉 ∈ (∟G‘𝐺)) |
41 | 37, 40 | eqeltrd 2688 |
. . . 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 25365 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐸)) = (𝐷 − 𝐸)) |
45 | 28 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐸)) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐸)) |
46 | 43, 44, 45 | 3eqtr2d 2650 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐵) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐸)) |
47 | 26 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐶)) |
48 | | eqid 2610 |
. . . 4
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(((pInvG‘𝐺)‘𝐵)‘𝐷))(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(((pInvG‘𝐺)‘𝐵)‘𝐷))(LineG‘𝐺)𝐵)) |
49 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → 𝐶 = 𝐶) |
50 | 1, 2, 3, 5, 7, 9, 11, 13, 19, 21, 13, 23, 41, 46, 47, 26, 48, 49 | hypcgrlem1 25491 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐶) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐶)) |
51 | 36 | oveq2d 6565 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − 𝐶) = ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐹))) |
52 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 31 | miriso 25365 |
. . 3
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → ((((pInvG‘𝐺)‘𝐵)‘𝐷) − (((pInvG‘𝐺)‘𝐵)‘𝐹)) = (𝐷 − 𝐹)) |
53 | 50, 51, 52 | 3eqtrd 2648 |
. 2
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) = 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
54 | 4 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐺 ∈ TarskiG) |
55 | 6 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐺DimTarskiG≥2) |
56 | 8 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐴 ∈ 𝑃) |
57 | 10 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐵 ∈ 𝑃) |
58 | 12 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐶 ∈ 𝑃) |
59 | 17 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐷 ∈ 𝑃) |
60 | 20 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐸 ∈ 𝑃) |
61 | 30 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐹 ∈ 𝑃) |
62 | 22 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
63 | 38 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
64 | 42 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
65 | | hypcgr.4 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
66 | 65 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
67 | 25 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐵 = 𝐸) |
68 | | eqid 2610 |
. . . 4
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) |
69 | | simpr 476 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → 𝐶 = 𝐹) |
70 | 1, 2, 3, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 66, 67, 68, 69 | hypcgrlem1 25491 |
. . 3
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = 𝐹) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
71 | 4 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐺 ∈ TarskiG) |
72 | 6 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐺DimTarskiG≥2) |
73 | 8 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐴 ∈ 𝑃) |
74 | 10 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ∈ 𝑃) |
75 | 12 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ∈ 𝑃) |
76 | | hypcgrlem2.s |
. . . . . 6
⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
77 | 30 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 ∈ 𝑃) |
78 | 1, 2, 3, 71, 72, 75, 77 | midcl 25469 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ 𝑃) |
79 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) |
80 | 1, 3, 14, 71, 78, 74, 79 | tgelrnln 25325 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∈ ran (LineG‘𝐺)) |
81 | 17 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐷 ∈ 𝑃) |
82 | 1, 2, 3, 71, 72, 76, 14, 80, 81 | lmicl 25478 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐷) ∈ 𝑃) |
83 | 20 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐸 ∈ 𝑃) |
84 | 1, 2, 3, 71, 72, 76, 14, 80, 83 | lmicl 25478 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐸) ∈ 𝑃) |
85 | 1, 2, 3, 71, 72, 76, 14, 80, 77 | lmicl 25478 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐹) ∈ 𝑃) |
86 | 22 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) |
87 | 1, 2, 3, 71, 72, 76, 14, 80 | lmimot 25490 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝑆 ∈ (𝐺Ismt𝐺)) |
88 | 38 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) |
89 | 1, 2, 3, 14, 15, 71, 81, 83, 77, 87, 88 | motrag 25403 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“(𝑆‘𝐷)(𝑆‘𝐸)(𝑆‘𝐹)”〉 ∈ (∟G‘𝐺)) |
90 | 42 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
91 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 83 | lmiiso 25489 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐷) − (𝑆‘𝐸)) = (𝐷 − 𝐸)) |
92 | 90, 91 | eqtr4d 2647 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐵) = ((𝑆‘𝐷) − (𝑆‘𝐸))) |
93 | 65 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
94 | 1, 2, 3, 71, 72, 76, 14, 80, 83, 77 | lmiiso 25489 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐸) − (𝑆‘𝐹)) = (𝐸 − 𝐹)) |
95 | 93, 94 | eqtr4d 2647 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = ((𝑆‘𝐸) − (𝑆‘𝐹))) |
96 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx2 25329 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
97 | 1, 2, 3, 71, 72, 76, 14, 80, 74 | lmiinv 25484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐵) = 𝐵 ↔ 𝐵 ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵))) |
98 | 96, 97 | mpbird 246 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐵) = 𝐵) |
99 | 25 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 = 𝐸) |
100 | 99 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝑆‘𝐵) = (𝑆‘𝐸)) |
101 | 98, 100 | eqtr3d 2646 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 = (𝑆‘𝐸)) |
102 | | eqid 2610 |
. . . . 5
⊢
((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑆‘𝐷))(LineG‘𝐺)𝐵)) = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑆‘𝐷))(LineG‘𝐺)𝐵)) |
103 | 1, 2, 3, 71, 72, 75, 77 | midcom 25474 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) = (𝐹(midG‘𝐺)𝐶)) |
104 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx1 25328 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
105 | 103, 104 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹(midG‘𝐺)𝐶) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) |
106 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ≠ 𝐹) |
107 | 106 | necomd 2837 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 ≠ 𝐶) |
108 | 1, 3, 14, 71, 77, 75, 107 | tgelrnln 25325 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹(LineG‘𝐺)𝐶) ∈ ran (LineG‘𝐺)) |
109 | 1, 2, 3, 71, 72, 75, 77 | midbtwn 25471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐶𝐼𝐹)) |
110 | 1, 2, 3, 71, 75, 78, 77, 109 | tgbtwncom 25183 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐹𝐼𝐶)) |
111 | 1, 3, 14, 71, 77, 75, 78, 107, 110 | btwnlng1 25314 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (𝐹(LineG‘𝐺)𝐶)) |
112 | 104, 111 | elind 3760 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) ∈ (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∩ (𝐹(LineG‘𝐺)𝐶))) |
113 | 1, 3, 14, 71, 77, 75, 107 | tglinerflx2 25329 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ∈ (𝐹(LineG‘𝐺)𝐶)) |
114 | 79 | necomd 2837 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐵 ≠ (𝐶(midG‘𝐺)𝐹)) |
115 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐺 ∈ TarskiG) |
116 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 ∈ 𝑃) |
117 | 30 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐹 ∈ 𝑃) |
118 | 6 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐺DimTarskiG≥2) |
119 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 = (𝐶(midG‘𝐺)𝐹)) |
120 | 119 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶(midG‘𝐺)𝐹) = 𝐶) |
121 | 1, 2, 3, 115, 118, 116, 117, 120 | midcgr 25472 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶 − 𝐶) = (𝐶 − 𝐹)) |
122 | 121 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → (𝐶 − 𝐹) = (𝐶 − 𝐶)) |
123 | 1, 2, 3, 115, 116, 117, 116, 122 | axtgcgrid 25162 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 = (𝐶(midG‘𝐺)𝐹)) → 𝐶 = 𝐹) |
124 | 123 | ex 449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐶 = (𝐶(midG‘𝐺)𝐹) → 𝐶 = 𝐹)) |
125 | 124 | necon3d 2803 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐶 ≠ 𝐹 → 𝐶 ≠ (𝐶(midG‘𝐺)𝐹))) |
126 | 125 | imp 444 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 ≠ (𝐶(midG‘𝐺)𝐹)) |
127 | 99 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐸 = 𝐵) |
128 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶(midG‘𝐺)𝐹) = (𝐶(midG‘𝐺)𝐹)) |
129 | 1, 2, 3, 71, 72, 75, 77, 15, 78 | ismidb 25470 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐹 = (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶) ↔ (𝐶(midG‘𝐺)𝐹) = (𝐶(midG‘𝐺)𝐹))) |
130 | 128, 129 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐹 = (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶)) |
131 | 127, 130 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐸 − 𝐹) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶))) |
132 | 93, 131 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐵 − 𝐶) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶))) |
133 | 1, 2, 3, 14, 15, 71, 74, 78, 75 | israg 25392 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (〈“𝐵(𝐶(midG‘𝐺)𝐹)𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐵 − 𝐶) = (𝐵 − (((pInvG‘𝐺)‘(𝐶(midG‘𝐺)𝐹))‘𝐶)))) |
134 | 132, 133 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 〈“𝐵(𝐶(midG‘𝐺)𝐹)𝐶”〉 ∈ (∟G‘𝐺)) |
135 | 1, 2, 3, 14, 71, 80, 108, 112, 96, 113, 114, 126, 134 | ragperp 25412 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶)) |
136 | 135 | orcd 406 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶) ∨ 𝐹 = 𝐶)) |
137 | 1, 2, 3, 71, 72, 76, 14, 80, 77, 75 | islmib 25479 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐶 = (𝑆‘𝐹) ↔ ((𝐹(midG‘𝐺)𝐶) ∈ ((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵) ∧ (((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)(⟂G‘𝐺)(𝐹(LineG‘𝐺)𝐶) ∨ 𝐹 = 𝐶)))) |
138 | 105, 136,
137 | mpbir2and 959 |
. . . . 5
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → 𝐶 = (𝑆‘𝐹)) |
139 | 1, 2, 3, 71, 72, 73, 74, 75, 82, 84, 85, 86, 89, 92, 95, 101, 102, 138 | hypcgrlem1 25491 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐶) = ((𝑆‘𝐷) − (𝑆‘𝐹))) |
140 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 77 | lmiiso 25489 |
. . . 4
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → ((𝑆‘𝐷) − (𝑆‘𝐹)) = (𝐷 − 𝐹)) |
141 | 139, 140 | eqtrd 2644 |
. . 3
⊢ (((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) ∧ 𝐶 ≠ 𝐹) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
142 | 70, 141 | pm2.61dane 2869 |
. 2
⊢ ((𝜑 ∧ (𝐶(midG‘𝐺)𝐹) ≠ 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
143 | 53, 142 | pm2.61dane 2869 |
1
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |