perpcom

Description: The "perpendicular" relation commutes. Theorem 8.12 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-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$
	isperp.b	$⊢ φ \to B \in ran L$
	perpcom.1	$⊢ φ \to A ⟂_{𝒢} (G) B$
Assertion	perpcom	$⊢ φ \to B ⟂_{𝒢} (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		isperp.b	$⊢ φ \to B \in ran L$
8		perpcom.1	$⊢ φ \to A ⟂_{𝒢} (G) B$
9		incom	$⊢ A \cap B = B \cap A$
10	9	a1i	$⊢ φ \to A \cap B = B \cap A$
11		ralcom	$⊢ \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \forall v \in B \forall u \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
12		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
13	5	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to G \in 𝒢_{Tarski}$
14	6	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to A \in ran L$
15		simplrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to u \in A$
16	1 4 3 13 14 15	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to u \in P$
17		simpllr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to x \in (A \cap B)$
18	17	elin1d	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to x \in A$
19	1 4 3 13 14 18	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to x \in P$
20	7	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to B \in ran L$
21		simplrl	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to v \in B$
22	1 4 3 13 20 21	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to v \in P$
23		simpr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
24	1 2 3 4 12 13 16 19 22 23	ragcom	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)$
25	5	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to G \in 𝒢_{Tarski}$
26	7	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to B \in ran L$
27		simplrl	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to v \in B$
28	1 4 3 25 26 27	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to v \in P$
29	6	ad3antrrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to A \in ran L$
30		simpllr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to x \in (A \cap B)$
31	30	elin1d	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to x \in A$
32	1 4 3 25 29 31	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to x \in P$
33		simplrr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to u \in A$
34	1 4 3 25 29 33	tglnpt	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to u \in P$
35		simpr	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)$
36	1 2 3 4 12 25 28 32 34 35	ragcom	$⊢ (((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \land ⟨“ v x u ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
37	24 36	impbida	$⊢ ((φ \land x \in (A \cap B)) \land (v \in B \land u \in A)) \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ v x u ”⟩ \in ∟_{𝒢} (G))$
38	37	2ralbidva	$⊢ (φ \land x \in (A \cap B)) \to (\forall v \in B \forall u \in A ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \forall v \in B \forall u \in A ⟨“ v x u ”⟩ \in ∟_{𝒢} (G))$
39	11 38	bitrid	$⊢ (φ \land x \in (A \cap B)) \to (\forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \forall v \in B \forall u \in A ⟨“ v x u ”⟩ \in ∟_{𝒢} (G))$
40	10 39	rexeqbidva	$⊢ φ \to (\exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \exists x \in (B \cap A) \forall v \in B \forall u \in A ⟨“ v x u ”⟩ \in ∟_{𝒢} (G))$
41	1 2 3 4 5 6 7	isperp	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
42	1 2 3 4 5 7 6	isperp	$⊢ φ \to (B ⟂_{𝒢} (G) A \leftrightarrow \exists x \in (B \cap A) \forall v \in B \forall u \in A ⟨“ v x u ”⟩ \in ∟_{𝒢} (G))$
43	40 41 42	3bitr4d	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow B ⟂_{𝒢} (G) A)$
44	8 43	mpbid	$⊢ φ \to B ⟂_{𝒢} (G) A$

Metamath Proof Explorer

Theorem perpcom

Proof