| Step | Hyp | Ref
| Expression |
| 1 | | tgcgrxfr.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐴 ∈ 𝑃) |
| 3 | | tgcgrxfr.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
| 4 | | tgcgrxfr.m |
. . . 4
⊢ − =
(dist‘𝐺) |
| 5 | | tgcgrxfr.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
| 6 | | tgcgrxfr.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐺 ∈ TarskiG) |
| 8 | | tgcgrxfr.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐷 ∈ 𝑃) |
| 10 | | tgcgrxfr.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐹 ∈ 𝑃) |
| 12 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) →
(♯‘𝑃) =
1) |
| 13 | 3, 4, 5, 7, 2, 9, 11, 12 | tgldim0itv 28512 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐴 ∈ (𝐷𝐼𝐹)) |
| 14 | | tgcgrxfr.r |
. . . 4
⊢ ∼ =
(cgrG‘𝐺) |
| 15 | | tgcgrxfr.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐵 ∈ 𝑃) |
| 17 | | tgcgrxfr.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐶 ∈ 𝑃) |
| 19 | 3, 4, 5, 7, 2, 16,
9, 12, 2 | tgldim0cgr 28513 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐴 − 𝐵) = (𝐷 − 𝐴)) |
| 20 | 3, 4, 5, 7, 16, 18, 2, 12, 11 | tgldim0cgr 28513 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐵 − 𝐶) = (𝐴 − 𝐹)) |
| 21 | 3, 4, 5, 7, 18, 2,
11, 12, 9 | tgldim0cgr 28513 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 22 | 3, 4, 14, 7, 2, 16, 18, 9, 2, 11, 19, 20, 21 | trgcgr 28524 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐴𝐹”〉) |
| 23 | | eleq1 2829 |
. . . . 5
⊢ (𝑒 = 𝐴 → (𝑒 ∈ (𝐷𝐼𝐹) ↔ 𝐴 ∈ (𝐷𝐼𝐹))) |
| 24 | | s3eq2 14909 |
. . . . . 6
⊢ (𝑒 = 𝐴 → 〈“𝐷𝑒𝐹”〉 = 〈“𝐷𝐴𝐹”〉) |
| 25 | 24 | breq2d 5155 |
. . . . 5
⊢ (𝑒 = 𝐴 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉 ↔ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐴𝐹”〉)) |
| 26 | 23, 25 | anbi12d 632 |
. . . 4
⊢ (𝑒 = 𝐴 → ((𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉) ↔ (𝐴 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐴𝐹”〉))) |
| 27 | 26 | rspcev 3622 |
. . 3
⊢ ((𝐴 ∈ 𝑃 ∧ (𝐴 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐴𝐹”〉)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 28 | 2, 13, 22, 27 | syl12anc 837 |
. 2
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 29 | 6 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → 𝐺 ∈ TarskiG) |
| 30 | | simplr 769 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → 𝑔 ∈ 𝑃) |
| 31 | 8 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → 𝐷 ∈ 𝑃) |
| 32 | 1 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → 𝐴 ∈ 𝑃) |
| 33 | 15 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → 𝐵 ∈ 𝑃) |
| 34 | 3, 4, 5, 29, 30, 31, 32, 33 | axtgsegcon 28472 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → ∃𝑒 ∈ 𝑃 (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) |
| 35 | 6 | ad7antr 738 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐺 ∈ TarskiG) |
| 36 | 30 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → 𝑔 ∈ 𝑃) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑔 ∈ 𝑃) |
| 38 | 8 | ad7antr 738 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ 𝑃) |
| 39 | | simplr 769 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → 𝑒 ∈ 𝑃) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑒 ∈ 𝑃) |
| 41 | | simplr 769 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ 𝑃) |
| 42 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) |
| 43 | 42 | simpld 494 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ (𝑔𝐼𝑒)) |
| 44 | | simprl 771 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑒 ∈ (𝑔𝐼𝑓)) |
| 45 | 3, 4, 5, 35, 37, 38, 40, 41, 43, 44 | tgbtwnexch3 28502 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑒 ∈ (𝐷𝐼𝑓)) |
| 46 | 1 | ad7antr 738 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐴 ∈ 𝑃) |
| 47 | 17 | ad7antr 738 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐶 ∈ 𝑃) |
| 48 | 10 | ad7antr 738 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ 𝑃) |
| 49 | | simp-5r 786 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) |
| 50 | 49 | simprd 495 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ≠ 𝑔) |
| 51 | 50 | necomd 2996 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑔 ≠ 𝐷) |
| 52 | 3, 4, 5, 35, 37, 38, 40, 41, 43, 44 | tgbtwnexch 28506 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ (𝑔𝐼𝑓)) |
| 53 | 49 | simpld 494 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ (𝐹𝐼𝑔)) |
| 54 | 3, 4, 5, 35, 48, 38, 37, 53 | tgbtwncom 28496 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ (𝑔𝐼𝐹)) |
| 55 | 15 | ad7antr 738 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐵 ∈ 𝑃) |
| 56 | | tgcgrxfr.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 57 | 56 | ad7antr 738 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 58 | 42 | simprd 495 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷 − 𝑒) = (𝐴 − 𝐵)) |
| 59 | | simprr 773 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝑒 − 𝑓) = (𝐵 − 𝐶)) |
| 60 | 3, 4, 5, 35, 38, 40, 41, 46, 55, 47, 45, 57, 58, 59 | tgcgrextend 28493 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷 − 𝑓) = (𝐴 − 𝐶)) |
| 61 | | tgcgrxfr.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 62 | 61 | ad7antr 738 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 63 | 62 | eqcomd 2743 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷 − 𝐹) = (𝐴 − 𝐶)) |
| 64 | 3, 4, 5, 35, 38, 46, 47, 37, 41, 48, 51, 52, 54, 60, 63 | tgsegconeq 28494 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 = 𝐹) |
| 65 | 64 | oveq2d 7447 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐷𝐼𝑓) = (𝐷𝐼𝐹)) |
| 66 | 45, 65 | eleqtrd 2843 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 𝑒 ∈ (𝐷𝐼𝐹)) |
| 67 | 58 | eqcomd 2743 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐵) = (𝐷 − 𝑒)) |
| 68 | 64 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝑒 − 𝑓) = (𝑒 − 𝐹)) |
| 69 | 59, 68 | eqtr3d 2779 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐶) = (𝑒 − 𝐹)) |
| 70 | 3, 4, 5, 6, 1, 17,
8, 10, 61 | tgcgrcomlr 28488 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 71 | 70 | ad7antr 738 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 72 | 3, 4, 14, 35, 46, 55, 47, 38, 40, 48, 67, 69, 71 | trgcgr 28524 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉) |
| 73 | 66, 72 | jca 511 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) ∧ 𝑓 ∈ 𝑃) ∧ (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) → (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 74 | 29 | ad2antrr 726 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → 𝐺 ∈ TarskiG) |
| 75 | 33 | ad2antrr 726 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → 𝐵 ∈ 𝑃) |
| 76 | 17 | ad5antr 734 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → 𝐶 ∈ 𝑃) |
| 77 | 3, 4, 5, 74, 36, 39, 75, 76 | axtgsegcon 28472 |
. . . . . . 7
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → ∃𝑓 ∈ 𝑃 (𝑒 ∈ (𝑔𝐼𝑓) ∧ (𝑒 − 𝑓) = (𝐵 − 𝐶))) |
| 78 | 73, 77 | r19.29a 3162 |
. . . . . 6
⊢
((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵))) → (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 79 | 78 | ex 412 |
. . . . 5
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) ∧ 𝑒 ∈ 𝑃) → ((𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵)) → (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉))) |
| 80 | 79 | reximdva 3168 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → (∃𝑒 ∈ 𝑃 (𝐷 ∈ (𝑔𝐼𝑒) ∧ (𝐷 − 𝑒) = (𝐴 − 𝐵)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉))) |
| 81 | 34, 80 | mpd 15 |
. . 3
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑔 ∈ 𝑃) ∧ (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 82 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐺 ∈ TarskiG) |
| 83 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐹 ∈ 𝑃) |
| 84 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐷 ∈ 𝑃) |
| 85 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 2 ≤
(♯‘𝑃)) |
| 86 | 3, 4, 5, 82, 83, 84, 85 | tgbtwndiff 28514 |
. . 3
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ∃𝑔 ∈ 𝑃 (𝐷 ∈ (𝐹𝐼𝑔) ∧ 𝐷 ≠ 𝑔)) |
| 87 | 81, 86 | r19.29a 3162 |
. 2
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |
| 88 | 3, 1 | tgldimor 28510 |
. 2
⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤
(♯‘𝑃))) |
| 89 | 28, 87, 88 | mpjaodan 961 |
1
⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) |