ragperp

Description: Deduce that two lines are perpendicular from a right angle statement. One direction of theorem 8.13 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 20-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$
	ragperp.b	$⊢ φ \to B \in ran L$
	ragperp.x	$⊢ φ \to X \in (A \cap B)$
	ragperp.u	$⊢ φ \to U \in A$
	ragperp.v	$⊢ φ \to V \in B$
	ragperp.1	$⊢ φ \to U \neq X$
	ragperp.2	$⊢ φ \to V \neq X$
	ragperp.r	$⊢ φ \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G)$
Assertion	ragperp	$⊢ φ \to A ⟂_{𝒢} (G) B$

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		ragperp.b	$⊢ φ \to B \in ran L$
8		ragperp.x	$⊢ φ \to X \in (A \cap B)$
9		ragperp.u	$⊢ φ \to U \in A$
10		ragperp.v	$⊢ φ \to V \in B$
11		ragperp.1	$⊢ φ \to U \neq X$
12		ragperp.2	$⊢ φ \to V \neq X$
13		ragperp.r	$⊢ φ \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G)$
14		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
15	5	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to G \in 𝒢_{Tarski}$
16	7	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to B \in ran L$
17		simprr	$⊢ (φ \land (u \in A \land v \in B)) \to v \in B$
18	1 4 3 15 16 17	tglnpt	$⊢ (φ \land (u \in A \land v \in B)) \to v \in P$
19	6	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to A \in ran L$
20	8	elin1d	$⊢ φ \to X \in A$
21	20	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to X \in A$
22	1 4 3 15 19 21	tglnpt	$⊢ (φ \land (u \in A \land v \in B)) \to X \in P$
23		simprl	$⊢ (φ \land (u \in A \land v \in B)) \to u \in A$
24	1 4 3 15 19 23	tglnpt	$⊢ (φ \land (u \in A \land v \in B)) \to u \in P$
25	10	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to V \in B$
26	1 4 3 15 16 25	tglnpt	$⊢ (φ \land (u \in A \land v \in B)) \to V \in P$
27	9	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to U \in A$
28	1 4 3 15 19 27	tglnpt	$⊢ (φ \land (u \in A \land v \in B)) \to U \in P$
29	13	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to ⟨“ U X V ”⟩ \in ∟_{𝒢} (G)$
30	11	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to U \neq X$
31	9	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to U \in A$
32	5	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to G \in 𝒢_{Tarski}$
33	22	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to X \in P$
34	24	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to u \in P$
35		simpr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to \neg X = u$
36	35	neqned	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to X \neq u$
37	6	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to A \in ran L$
38	20	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to X \in A$
39	23	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to u \in A$
40	1 3 4 32 33 34 36 36 37 38 39	tglinethru	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to A = X L u$
41	31 40	eleqtrd	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = u) \to U \in (X L u)$
42	41	ex	$⊢ (φ \land (u \in A \land v \in B)) \to (\neg X = u \to U \in (X L u))$
43	42	orrd	$⊢ (φ \land (u \in A \land v \in B)) \to (X = u \lor U \in (X L u))$
44	43	orcomd	$⊢ (φ \land (u \in A \land v \in B)) \to (U \in (X L u) \lor X = u)$
45	1 2 3 4 14 15 28 22 26 24 29 30 44	ragcol	$⊢ (φ \land (u \in A \land v \in B)) \to ⟨“ u X V ”⟩ \in ∟_{𝒢} (G)$
46	1 2 3 4 14 15 24 22 26 45	ragcom	$⊢ (φ \land (u \in A \land v \in B)) \to ⟨“ V X u ”⟩ \in ∟_{𝒢} (G)$
47	12	adantr	$⊢ (φ \land (u \in A \land v \in B)) \to V \neq X$
48	10	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to V \in B$
49	5	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to G \in 𝒢_{Tarski}$
50	22	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to X \in P$
51	18	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to v \in P$
52		simpr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to \neg X = v$
53	52	neqned	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to X \neq v$
54	7	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to B \in ran L$
55	8	elin2d	$⊢ φ \to X \in B$
56	55	ad2antrr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to X \in B$
57	17	adantr	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to v \in B$
58	1 3 4 49 50 51 53 53 54 56 57	tglinethru	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to B = X L v$
59	48 58	eleqtrd	$⊢ ((φ \land (u \in A \land v \in B)) \land \neg X = v) \to V \in (X L v)$
60	59	ex	$⊢ (φ \land (u \in A \land v \in B)) \to (\neg X = v \to V \in (X L v))$
61	60	orrd	$⊢ (φ \land (u \in A \land v \in B)) \to (X = v \lor V \in (X L v))$
62	61	orcomd	$⊢ (φ \land (u \in A \land v \in B)) \to (V \in (X L v) \lor X = v)$
63	1 2 3 4 14 15 26 22 24 18 46 47 62	ragcol	$⊢ (φ \land (u \in A \land v \in B)) \to ⟨“ v X u ”⟩ \in ∟_{𝒢} (G)$
64	1 2 3 4 14 15 18 22 24 63	ragcom	$⊢ (φ \land (u \in A \land v \in B)) \to ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)$
65	64	ralrimivva	$⊢ φ \to \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)$
66	1 2 3 4 5 6 7 8	isperp2	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
67	65 66	mpbird	$⊢ φ \to A ⟂_{𝒢} (G) B$

Metamath Proof Explorer

Theorem ragperp

Proof