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 ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ( 𝐹 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐵 𝐼 𝐸 ) ) )