Step | Hyp | Ref
| Expression |
1 | | tkgeom.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | tkgeom.d |
. . . 4
⊢ − =
(dist‘𝐺) |
3 | | tkgeom.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
4 | | tkgeom.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐺 ∈ TarskiG) |
6 | | tgtrisegint.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
7 | 6 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐸 ∈ 𝑃) |
8 | | tgbtwnintr.3 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
9 | 8 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐶 ∈ 𝑃) |
10 | | tgbtwnintr.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
11 | 10 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐴 ∈ 𝑃) |
12 | | simplr 788 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝑟 ∈ 𝑃) |
13 | | tgbtwnintr.2 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
14 | 13 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐵 ∈ 𝑃) |
15 | | simprl 790 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝑟 ∈ (𝐸𝐼𝐴)) |
16 | | tgtrisegint.1 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
17 | 16 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐵 ∈ (𝐴𝐼𝐶)) |
18 | 1, 2, 3, 5, 11, 14, 9, 17 | tgbtwncom 25183 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐵 ∈ (𝐶𝐼𝐴)) |
19 | 1, 2, 3, 5, 7, 9, 11, 12, 14, 15, 18 | axtgpasch 25166 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝑟𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸))) |
20 | 5 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝐺 ∈ TarskiG) |
21 | | tgtrisegint.p |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
22 | 21 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝐹 ∈ 𝑃) |
23 | 22 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝐹 ∈ 𝑃) |
24 | 12 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝑟 ∈ 𝑃) |
25 | | simplr 788 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝑞 ∈ 𝑃) |
26 | 9 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝐶 ∈ 𝑃) |
27 | | simprr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → 𝑟 ∈ (𝐹𝐼𝐶)) |
28 | 27 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝑟 ∈ (𝐹𝐼𝐶)) |
29 | | simpr 476 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝑞 ∈ (𝑟𝐼𝐶)) |
30 | 1, 2, 3, 20, 23, 24, 25, 26, 28, 29 | tgbtwnexch2 25191 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) ∧ 𝑞 ∈ (𝑟𝐼𝐶)) → 𝑞 ∈ (𝐹𝐼𝐶)) |
31 | 30 | ex 449 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) → (𝑞 ∈ (𝑟𝐼𝐶) → 𝑞 ∈ (𝐹𝐼𝐶))) |
32 | 31 | anim1d 586 |
. . . 4
⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) ∧ 𝑞 ∈ 𝑃) → ((𝑞 ∈ (𝑟𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸)) → (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸)))) |
33 | 32 | reximdva 3000 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → (∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝑟𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸)) → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸)))) |
34 | 19, 33 | mpd 15 |
. 2
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸))) |
35 | | tgbtwnintr.4 |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
36 | | tgtrisegint.2 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐶)) |
37 | 1, 2, 3, 4, 35, 6,
8, 36 | tgbtwncom 25183 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (𝐶𝐼𝐷)) |
38 | | tgtrisegint.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐷)) |
39 | 1, 2, 3, 4, 8, 10,
35, 6, 21, 37, 38 | axtgpasch 25166 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐸𝐼𝐴) ∧ 𝑟 ∈ (𝐹𝐼𝐶))) |
40 | 34, 39 | r19.29a 3060 |
1
⊢ (𝜑 → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸))) |