MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgtrisegint Structured version   Visualization version   Unicode version

Theorem tgtrisegint 24543
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.)
Hypotheses
Ref Expression
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
Ref Expression
tgtrisegint  |-  ( ph  ->  E. q  e.  P  ( q  e.  ( F I C )  /\  q  e.  ( B I E ) ) )
Distinct variable groups:    .- , q    A, q    B, q    C, q    D, q    E, q    F, q    I, q    P, q    ph, q
Allowed substitution hint:    G( q)

Proof of Theorem tgtrisegint
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 tkgeom.p . . . 4  |-  P  =  ( Base `  G
)
2 tkgeom.d . . . 4  |-  .-  =  ( dist `  G )
3 tkgeom.i . . . 4  |-  I  =  (Itv `  G )
4 tkgeom.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
54ad2antrr 732 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  G  e. TarskiG )
6 tgtrisegint.e . . . . 5  |-  ( ph  ->  E  e.  P )
76ad2antrr 732 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  E  e.  P
)
8 tgbtwnintr.3 . . . . 5  |-  ( ph  ->  C  e.  P )
98ad2antrr 732 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  C  e.  P
)
10 tgbtwnintr.1 . . . . 5  |-  ( ph  ->  A  e.  P )
1110ad2antrr 732 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  A  e.  P
)
12 simplr 762 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  r  e.  P
)
13 tgbtwnintr.2 . . . . 5  |-  ( ph  ->  B  e.  P )
1413ad2antrr 732 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  B  e.  P
)
15 simprl 764 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  r  e.  ( E I A ) )
16 tgtrisegint.1 . . . . . 6  |-  ( ph  ->  B  e.  ( A I C ) )
1716ad2antrr 732 . . . . 5  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  B  e.  ( A I C ) )
181, 2, 3, 5, 11, 14, 9, 17tgbtwncom 24532 . . . 4  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  B  e.  ( C I A ) )
191, 2, 3, 5, 7, 9, 11, 12, 14, 15, 18axtgpasch 24515 . . 3  |-  ( ( ( 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 ) ) )
205ad2antrr 732 . . . . . . 7  |-  ( ( ( ( ( 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 )
21 tgtrisegint.p . . . . . . . . 9  |-  ( ph  ->  F  e.  P )
2221ad2antrr 732 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  F  e.  P
)
2322ad2antrr 732 . . . . . . 7  |-  ( ( ( ( ( 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 )
2412ad2antrr 732 . . . . . . 7  |-  ( ( ( ( ( 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 )
25 simplr 762 . . . . . . 7  |-  ( ( ( ( ( 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 )
269ad2antrr 732 . . . . . . 7  |-  ( ( ( ( ( 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 )
27 simprr 766 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )  ->  r  e.  ( F I C ) )
2827ad2antrr 732 . . . . . . 7  |-  ( ( ( ( ( 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 ) )
29 simpr 463 . . . . . . 7  |-  ( ( ( ( ( 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 ) )
301, 2, 3, 20, 23, 24, 25, 26, 28, 29tgbtwnexch2 24540 . . . . . 6  |-  ( ( ( ( ( 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 ) )
3130ex 436 . . . . 5  |-  ( ( ( ( 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 ) ) )
3231anim1d 568 . . . 4  |-  ( ( ( ( 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 ) ) ) )
3332reximdva 2862 . . 3  |-  ( ( ( 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 ) ) ) )
3419, 33mpd 15 . 2  |-  ( ( ( 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 ) ) )
35 tgbtwnintr.4 . . 3  |-  ( ph  ->  D  e.  P )
36 tgtrisegint.2 . . . 4  |-  ( ph  ->  E  e.  ( D I C ) )
371, 2, 3, 4, 35, 6, 8, 36tgbtwncom 24532 . . 3  |-  ( ph  ->  E  e.  ( C I D ) )
38 tgtrisegint.3 . . 3  |-  ( ph  ->  F  e.  ( A I D ) )
391, 2, 3, 4, 8, 10, 35, 6, 21, 37, 38axtgpasch 24515 . 2  |-  ( ph  ->  E. r  e.  P  ( r  e.  ( E I A )  /\  r  e.  ( F I C ) ) )
4034, 39r19.29a 2932 1  |-  ( ph  ->  E. q  e.  P  ( q  e.  ( F I C )  /\  q  e.  ( B I E ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    e. wcel 1887   E.wrex 2738   ` cfv 5582  (class class class)co 6290   Basecbs 15121   distcds 15199  TarskiGcstrkg 24478  Itvcitv 24484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-nul 4534
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293  df-trkgc 24496  df-trkgb 24497  df-trkgcb 24498  df-trkg 24501
This theorem is referenced by:  krippenlem  24735  colperpexlem3  24774
  Copyright terms: Public domain W3C validator