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 = ( Base ` G )
tkgeom.d 
|- .- = ( dist ` G )
tkgeom.i 
|- I = ( Itv ` G )
tkgeom.g 
|- ( ph -> G e. TarskiG )
tgbtwnintr.1 
|- ( ph -> A e. P )
tgbtwnintr.2 
|- ( ph -> B e. P )
tgbtwnintr.3 
|- ( ph -> C e. P )
tgbtwnintr.4 
|- ( ph -> D e. P )
tgtrisegint.e 
|- ( ph -> E e. P )
tgtrisegint.p 
|- ( ph -> F e. P )
tgtrisegint.1 
|- ( ph -> B e. ( A I C ) )
tgtrisegint.2 
|- ( ph -> E e. ( D I C ) )
tgtrisegint.3 
|- ( ph -> F e. ( A I D ) )
Assertion tgtrisegint 
|- ( ph -> E. q e. P ( q e. ( F I C ) /\ q e. ( B I E ) ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 
 |-  P = ( Base ` G )
2 tkgeom.d 
 |-  .- = ( dist ` G )
3 tkgeom.i 
 |-  I = ( Itv ` G )
4 tkgeom.g 
 |-  ( ph -> G e. TarskiG )
5 tgbtwnintr.1 
 |-  ( ph -> A e. P )
6 tgbtwnintr.2 
 |-  ( ph -> B e. P )
7 tgbtwnintr.3 
 |-  ( ph -> C e. P )
8 tgbtwnintr.4 
 |-  ( ph -> D e. P )
9 tgtrisegint.e 
 |-  ( ph -> E e. P )
10 tgtrisegint.p 
 |-  ( ph -> F e. P )
11 tgtrisegint.1 
 |-  ( ph -> B e. ( A I C ) )
12 tgtrisegint.2 
 |-  ( ph -> E e. ( D I C ) )
13 tgtrisegint.3 
 |-  ( ph -> F e. ( A I D ) )
14 4 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> G e. TarskiG )
15 9 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> E e. P )
16 7 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> C e. P )
17 5 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> A e. P )
18 simplr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> r e. P )
19 6 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> B e. P )
20 simprl 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> r e. ( E I A ) )
21 11 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> B e. ( A I C ) )
22 1 2 3 14 17 19 16 21 tgbtwncom 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> B e. ( C I A ) )
23 1 2 3 14 15 16 17 18 19 20 22 axtgpasch 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> E. q e. P ( q e. ( r I C ) /\ q e. ( B I E ) ) )
24 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> G e. TarskiG )
25 10 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> F e. P )
26 25 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> F e. P )
27 18 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> r e. P )
28 simplr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> q e. P )
29 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> C e. P )
30 simprr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> r e. ( F I C ) )
31 30 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> r e. ( F I C ) )
32 simpr 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> q e. ( r I C ) )
33 1 2 3 24 26 27 28 29 31 32 tgbtwnexch2 
 |-  ( ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) /\ q e. ( r I C ) ) -> q e. ( F I C ) )
34 33 ex 
 |-  ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) -> ( q e. ( r I C ) -> q e. ( F I C ) ) )
35 34 anim1d 
 |-  ( ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) /\ q e. P ) -> ( ( q e. ( r I C ) /\ q e. ( B I E ) ) -> ( q e. ( F I C ) /\ q e. ( B I E ) ) ) )
36 35 reximdva 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> ( E. q e. P ( q e. ( r I C ) /\ q e. ( B I E ) ) -> E. q e. P ( q e. ( F I C ) /\ q e. ( B I E ) ) ) )
37 23 36 mpd 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( E I A ) /\ r e. ( F I C ) ) ) -> E. q e. P ( q e. ( F I C ) /\ q e. ( B I E ) ) )
38 1 2 3 4 8 9 7 12 tgbtwncom 
 |-  ( ph -> E e. ( C I D ) )
39 1 2 3 4 7 5 8 9 10 38 13 axtgpasch 
 |-  ( ph -> E. r e. P ( r e. ( E I A ) /\ r e. ( F I C ) ) )
40 37 39 r19.29a 
 |-  ( ph -> E. q e. P ( q e. ( F I C ) /\ q e. ( B I E ) ) )