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
tkgeom.d
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
Ref Expression
tgtrisegint
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem tgtrisegint
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 tkgeom.p . . . 4
2 tkgeom.d . . . 4
3 tkgeom.i . . . 4 Itv
4 tkgeom.g . . . . 5 TarskiG
54ad2antrr 732 . . . 4 TarskiG
6 tgtrisegint.e . . . . 5
76ad2antrr 732 . . . 4
8 tgbtwnintr.3 . . . . 5
98ad2antrr 732 . . . 4
10 tgbtwnintr.1 . . . . 5
1110ad2antrr 732 . . . 4
12 simplr 762 . . . 4
13 tgbtwnintr.2 . . . . 5
1413ad2antrr 732 . . . 4
15 simprl 764 . . . 4
16 tgtrisegint.1 . . . . . 6
1716ad2antrr 732 . . . . 5
181, 2, 3, 5, 11, 14, 9, 17tgbtwncom 24532 . . . 4
191, 2, 3, 5, 7, 9, 11, 12, 14, 15, 18axtgpasch 24515 . . 3
205ad2antrr 732 . . . . . . 7 TarskiG
21 tgtrisegint.p . . . . . . . . 9
2221ad2antrr 732 . . . . . . . 8
2322ad2antrr 732 . . . . . . 7
2412ad2antrr 732 . . . . . . 7
25 simplr 762 . . . . . . 7
269ad2antrr 732 . . . . . . 7
27 simprr 766 . . . . . . . 8
2827ad2antrr 732 . . . . . . 7
29 simpr 463 . . . . . . 7
301, 2, 3, 20, 23, 24, 25, 26, 28, 29tgbtwnexch2 24540 . . . . . 6
3130ex 436 . . . . 5
3231anim1d 568 . . . 4
3332reximdva 2862 . . 3
3419, 33mpd 15 . 2
35 tgbtwnintr.4 . . 3
36 tgtrisegint.2 . . . 4
371, 2, 3, 4, 35, 6, 8, 36tgbtwncom 24532 . . 3
38 tgtrisegint.3 . . 3
391, 2, 3, 4, 8, 10, 35, 6, 21, 37, 38axtgpasch 24515 . 2
4034, 39r19.29a 2932 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1444   wcel 1887  wrex 2738  cfv 5582  (class class class)co 6290  cbs 15121  cds 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