foot

Description: From a point C outside of a line A , there exists a unique point x on A such that ( C L x ) is perpendicular to A . That point is called the foot from C on A . Theorem 8.18 of Schwabhauser p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019)

	Ref	Expression
Hypotheses	isperp.p	$⊢ P = {Base}_{G}$
	isperp.d	$⊢ \underset{˙}{-} = dist (G)$
	isperp.i	$⊢ I = Itv (G)$
	isperp.l	$⊢ L = {Line}_{𝒢} (G)$
	isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isperp.a	$⊢ φ \to A \in ran L$
	foot.x	$⊢ φ \to C \in P$
	foot.y	$⊢ φ \to \neg C \in A$
Assertion	foot	$⊢ φ \to \exists! x \in A (C L x) ⟂_{𝒢} (G) A$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$⊢ P = {Base}_{G}$
2		isperp.d	$⊢ \underset{˙}{-} = dist (G)$
3		isperp.i	$⊢ I = Itv (G)$
4		isperp.l	$⊢ L = {Line}_{𝒢} (G)$
5		isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		isperp.a	$⊢ φ \to A \in ran L$
7		foot.x	$⊢ φ \to C \in P$
8		foot.y	$⊢ φ \to \neg C \in A$
9	1 2 3 4 5 6 7 8	footex	$⊢ φ \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
10		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
11	5	ad2antrr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to G \in 𝒢_{Tarski}$
12	7	ad2antrr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to C \in P$
13	5	adantr	$⊢ (φ \land (x \in A \land z \in A)) \to G \in 𝒢_{Tarski}$
14	6	adantr	$⊢ (φ \land (x \in A \land z \in A)) \to A \in ran L$
15		simprl	$⊢ (φ \land (x \in A \land z \in A)) \to x \in A$
16	1 4 3 13 14 15	tglnpt	$⊢ (φ \land (x \in A \land z \in A)) \to x \in P$
17	16	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to x \in P$
18		simprr	$⊢ (φ \land (x \in A \land z \in A)) \to z \in A$
19	1 4 3 13 14 18	tglnpt	$⊢ (φ \land (x \in A \land z \in A)) \to z \in P$
20	19	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to z \in P$
21	8	adantr	$⊢ (φ \land (x \in A \land z \in A)) \to \neg C \in A$
22		nelne2	$⊢ (x \in A \land \neg C \in A) \to x \neq C$
23	15 21 22	syl2anc	$⊢ (φ \land (x \in A \land z \in A)) \to x \neq C$
24	23	necomd	$⊢ (φ \land (x \in A \land z \in A)) \to C \neq x$
25	24	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to C \neq x$
26	1 3 4 11 12 17 25	tglinerflx1	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to C \in (C L x)$
27	18	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to z \in A$
28		simprl	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to (C L x) ⟂_{𝒢} (G) A$
29	7	adantr	$⊢ (φ \land (x \in A \land z \in A)) \to C \in P$
30	1 3 4 13 29 16 24	tgelrnln	$⊢ (φ \land (x \in A \land z \in A)) \to C L x \in ran L$
31	1 3 4 13 29 16 24	tglinerflx2	$⊢ (φ \land (x \in A \land z \in A)) \to x \in (C L x)$
32	31 15	elind	$⊢ (φ \land (x \in A \land z \in A)) \to x \in ((C L x) \cap A)$
33	1 2 3 4 13 30 14 32	isperp2	$⊢ (φ \land (x \in A \land z \in A)) \to ((C L x) ⟂_{𝒢} (G) A \leftrightarrow \forall u \in (C L x) \forall v \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
34	33	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to ((C L x) ⟂_{𝒢} (G) A \leftrightarrow \forall u \in (C L x) \forall v \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
35	28 34	mpbid	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to \forall u \in (C L x) \forall v \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
36		id	$⊢ u = C \to u = C$
37		eqidd	$⊢ u = C \to x = x$
38		eqidd	$⊢ u = C \to v = v$
39	36 37 38	s3eqd	$⊢ u = C \to ⟨“ u x v ”⟩ = ⟨“ C x v ”⟩$
40	39	eleq1d	$⊢ u = C \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ C x v ”⟩ \in ∟_{𝒢} (G))$
41		eqidd	$⊢ v = z \to C = C$
42		eqidd	$⊢ v = z \to x = x$
43		id	$⊢ v = z \to v = z$
44	41 42 43	s3eqd	$⊢ v = z \to ⟨“ C x v ”⟩ = ⟨“ C x z ”⟩$
45	44	eleq1d	$⊢ v = z \to (⟨“ C x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ C x z ”⟩ \in ∟_{𝒢} (G))$
46	40 45	rspc2va	$⊢ ((C \in (C L x) \land z \in A) \land \forall u \in (C L x) \forall v \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ C x z ”⟩ \in ∟_{𝒢} (G)$
47	26 27 35 46	syl21anc	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to ⟨“ C x z ”⟩ \in ∟_{𝒢} (G)$
48		nelne2	$⊢ (z \in A \land \neg C \in A) \to z \neq C$
49	18 21 48	syl2anc	$⊢ (φ \land (x \in A \land z \in A)) \to z \neq C$
50	49	necomd	$⊢ (φ \land (x \in A \land z \in A)) \to C \neq z$
51	50	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to C \neq z$
52	1 3 4 11 12 20 51	tglinerflx1	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to C \in (C L z)$
53	15	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to x \in A$
54		simprr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to (C L z) ⟂_{𝒢} (G) A$
55	1 3 4 13 29 19 50	tgelrnln	$⊢ (φ \land (x \in A \land z \in A)) \to C L z \in ran L$
56	1 3 4 13 29 19 50	tglinerflx2	$⊢ (φ \land (x \in A \land z \in A)) \to z \in (C L z)$
57	56 18	elind	$⊢ (φ \land (x \in A \land z \in A)) \to z \in ((C L z) \cap A)$
58	1 2 3 4 13 55 14 57	isperp2	$⊢ (φ \land (x \in A \land z \in A)) \to ((C L z) ⟂_{𝒢} (G) A \leftrightarrow \forall u \in (C L z) \forall v \in A ⟨“ u z v ”⟩ \in ∟_{𝒢} (G))$
59	58	adantr	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to ((C L z) ⟂_{𝒢} (G) A \leftrightarrow \forall u \in (C L z) \forall v \in A ⟨“ u z v ”⟩ \in ∟_{𝒢} (G))$
60	54 59	mpbid	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to \forall u \in (C L z) \forall v \in A ⟨“ u z v ”⟩ \in ∟_{𝒢} (G)$
61		eqidd	$⊢ u = C \to z = z$
62	36 61 38	s3eqd	$⊢ u = C \to ⟨“ u z v ”⟩ = ⟨“ C z v ”⟩$
63	62	eleq1d	$⊢ u = C \to (⟨“ u z v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ C z v ”⟩ \in ∟_{𝒢} (G))$
64		eqidd	$⊢ v = x \to C = C$
65		eqidd	$⊢ v = x \to z = z$
66		id	$⊢ v = x \to v = x$
67	64 65 66	s3eqd	$⊢ v = x \to ⟨“ C z v ”⟩ = ⟨“ C z x ”⟩$
68	67	eleq1d	$⊢ v = x \to (⟨“ C z v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ C z x ”⟩ \in ∟_{𝒢} (G))$
69	63 68	rspc2va	$⊢ ((C \in (C L z) \land x \in A) \land \forall u \in (C L z) \forall v \in A ⟨“ u z v ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ C z x ”⟩ \in ∟_{𝒢} (G)$
70	52 53 60 69	syl21anc	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to ⟨“ C z x ”⟩ \in ∟_{𝒢} (G)$
71	1 2 3 4 10 11 12 17 20 47 70	ragflat	$⊢ ((φ \land (x \in A \land z \in A)) \land ((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A)) \to x = z$
72	71	ex	$⊢ (φ \land (x \in A \land z \in A)) \to (((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A) \to x = z)$
73	72	ralrimivva	$⊢ φ \to \forall x \in A \forall z \in A (((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A) \to x = z)$
74		oveq2	$⊢ x = z \to C L x = C L z$
75	74	breq1d	$⊢ x = z \to ((C L x) ⟂_{𝒢} (G) A \leftrightarrow (C L z) ⟂_{𝒢} (G) A)$
76	75	rmo4	$⊢ \exists^{*} x \in A (C L x) ⟂_{𝒢} (G) A \leftrightarrow \forall x \in A \forall z \in A (((C L x) ⟂_{𝒢} (G) A \land (C L z) ⟂_{𝒢} (G) A) \to x = z)$
77	73 76	sylibr	$⊢ φ \to \exists^{*} x \in A (C L x) ⟂_{𝒢} (G) A$
78		reu5	$⊢ \exists! x \in A (C L x) ⟂_{𝒢} (G) A \leftrightarrow (\exists x \in A (C L x) ⟂_{𝒢} (G) A \land \exists^{*} x \in A (C L x) ⟂_{𝒢} (G) A)$
79	9 77 78	sylanbrc	$⊢ φ \to \exists! x \in A (C L x) ⟂_{𝒢} (G) A$

Metamath Proof Explorer

Theorem foot

Proof