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	$⊢ \underset{˙}{-} = dist (G)$
	tkgeom.i	$⊢ I = Itv (G)$
	tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnintr.1	$⊢ φ \to A \in P$
	tgbtwnintr.2	$⊢ φ \to B \in P$
	tgbtwnintr.3	$⊢ φ \to C \in P$
	tgbtwnintr.4	$⊢ φ \to D \in P$
	tgtrisegint.e	$⊢ φ \to E \in P$
	tgtrisegint.p	$⊢ φ \to F \in P$
	tgtrisegint.1	$⊢ φ \to B \in (A I C)$
	tgtrisegint.2	$⊢ φ \to E \in (D I C)$
	tgtrisegint.3	$⊢ φ \to F \in (A I D)$
Assertion	tgtrisegint	$⊢ φ \to \exists q \in P (q \in (F I C) \land q \in (B I E))$

Proof

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

Metamath Proof Explorer

Theorem tgtrisegint

Proof