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 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnintr.1 ( 𝜑𝐴𝑃 )
tgbtwnintr.2 ( 𝜑𝐵𝑃 )
tgbtwnintr.3 ( 𝜑𝐶𝑃 )
tgbtwnintr.4 ( 𝜑𝐷𝑃 )
tgtrisegint.e ( 𝜑𝐸𝑃 )
tgtrisegint.p ( 𝜑𝐹𝑃 )
tgtrisegint.1 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgtrisegint.2 ( 𝜑𝐸 ∈ ( 𝐷 𝐼 𝐶 ) )
tgtrisegint.3 ( 𝜑𝐹 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgtrisegint ( 𝜑 → ∃ 𝑞𝑃 ( 𝑞 ∈ ( 𝐹 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐵 𝐼 𝐸 ) ) )

Proof

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