# Metamath Proof Explorer

## Theorem tgtrisegint

Description: A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of Schwabhauser p. 33. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tkgeom.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
tkgeom.d
tkgeom.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tkgeom.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
tgbtwnintr.1 ${⊢}{\phi }\to {A}\in {P}$
tgbtwnintr.2 ${⊢}{\phi }\to {B}\in {P}$
tgbtwnintr.3 ${⊢}{\phi }\to {C}\in {P}$
tgbtwnintr.4 ${⊢}{\phi }\to {D}\in {P}$
tgtrisegint.e ${⊢}{\phi }\to {E}\in {P}$
tgtrisegint.p ${⊢}{\phi }\to {F}\in {P}$
tgtrisegint.1 ${⊢}{\phi }\to {B}\in \left({A}{I}{C}\right)$
tgtrisegint.2 ${⊢}{\phi }\to {E}\in \left({D}{I}{C}\right)$
tgtrisegint.3 ${⊢}{\phi }\to {F}\in \left({A}{I}{D}\right)$
Assertion tgtrisegint ${⊢}{\phi }\to \exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({F}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 tkgeom.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 tkgeom.d
3 tkgeom.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 tkgeom.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 tgbtwnintr.1 ${⊢}{\phi }\to {A}\in {P}$
6 tgbtwnintr.2 ${⊢}{\phi }\to {B}\in {P}$
7 tgbtwnintr.3 ${⊢}{\phi }\to {C}\in {P}$
8 tgbtwnintr.4 ${⊢}{\phi }\to {D}\in {P}$
9 tgtrisegint.e ${⊢}{\phi }\to {E}\in {P}$
10 tgtrisegint.p ${⊢}{\phi }\to {F}\in {P}$
11 tgtrisegint.1 ${⊢}{\phi }\to {B}\in \left({A}{I}{C}\right)$
12 tgtrisegint.2 ${⊢}{\phi }\to {E}\in \left({D}{I}{C}\right)$
13 tgtrisegint.3 ${⊢}{\phi }\to {F}\in \left({A}{I}{D}\right)$
14 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
15 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {E}\in {P}$
16 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {C}\in {P}$
17 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {A}\in {P}$
18 simplr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {r}\in {P}$
19 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {B}\in {P}$
20 simprl ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {r}\in \left({E}{I}{A}\right)$
21 11 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {B}\in \left({A}{I}{C}\right)$
22 1 2 3 14 17 19 16 21 tgbtwncom ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {B}\in \left({C}{I}{A}\right)$
23 1 2 3 14 15 16 17 18 19 20 22 axtgpasch ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to \exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({r}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)$
24 14 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
25 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {F}\in {P}$
26 25 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {F}\in {P}$
27 18 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {r}\in {P}$
28 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {q}\in {P}$
29 16 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {C}\in {P}$
30 simprr ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to {r}\in \left({F}{I}{C}\right)$
31 30 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {r}\in \left({F}{I}{C}\right)$
32 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {q}\in \left({r}{I}{C}\right)$
33 1 2 3 24 26 27 28 29 31 32 tgbtwnexch2 ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\wedge {q}\in \left({r}{I}{C}\right)\right)\to {q}\in \left({F}{I}{C}\right)$
34 33 ex ${⊢}\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\to \left({q}\in \left({r}{I}{C}\right)\to {q}\in \left({F}{I}{C}\right)\right)$
35 34 anim1d ${⊢}\left(\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\wedge {q}\in {P}\right)\to \left(\left({q}\in \left({r}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)\to \left({q}\in \left({F}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)\right)$
36 35 reximdva ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to \left(\exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({r}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)\to \exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({F}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)\right)$
37 23 36 mpd ${⊢}\left(\left({\phi }\wedge {r}\in {P}\right)\wedge \left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)\right)\to \exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({F}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)$
38 1 2 3 4 8 9 7 12 tgbtwncom ${⊢}{\phi }\to {E}\in \left({C}{I}{D}\right)$
39 1 2 3 4 7 5 8 9 10 38 13 axtgpasch ${⊢}{\phi }\to \exists {r}\in {P}\phantom{\rule{.4em}{0ex}}\left({r}\in \left({E}{I}{A}\right)\wedge {r}\in \left({F}{I}{C}\right)\right)$
40 37 39 r19.29a ${⊢}{\phi }\to \exists {q}\in {P}\phantom{\rule{.4em}{0ex}}\left({q}\in \left({F}{I}{C}\right)\wedge {q}\in \left({B}{I}{E}\right)\right)$