perpneq

Description: Two perpendicular lines are different. Theorem 8.14 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 18-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	perpneq	$⊢ φ \to A \neq 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		isperp.b	$⊢ φ \to B \in ran L$
8		perpcom.1	$⊢ φ \to A ⟂_{𝒢} (G) B$
9	5	adantr	$⊢ (φ \land x \in (A \cap B)) \to G \in 𝒢_{Tarski}$
10	9	ad5antr	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to G \in 𝒢_{Tarski}$
11	5	ad5antr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to G \in 𝒢_{Tarski}$
12	6	ad5antr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to A \in ran L$
13		simpr	$⊢ (φ \land x \in (A \cap B)) \to x \in (A \cap B)$
14	13	elin1d	$⊢ (φ \land x \in (A \cap B)) \to x \in A$
15	14	ad4antr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \in A$
16	1 4 3 11 12 15	tglnpt	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \in P$
17	16	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \in P$
18	7	ad5antr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to B \in ran L$
19		simplr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \in B$
20	1 4 3 11 18 19	tglnpt	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \in P$
21	20	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \in P$
22		simp-4r	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \in A$
23	1 4 3 11 12 22	tglnpt	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \in P$
24	23	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \in P$
25		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
26		simp-4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \in A$
27		simplr	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \in B$
28		simp-5r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)$
29		id	$⊢ y = u \to y = u$
30		eqidd	$⊢ y = u \to x = x$
31		eqidd	$⊢ y = u \to z = z$
32	29 30 31	s3eqd	$⊢ y = u \to ⟨“ y x z ”⟩ = ⟨“ u x z ”⟩$
33	32	eleq1d	$⊢ y = u \to (⟨“ y x z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ u x z ”⟩ \in ∟_{𝒢} (G))$
34		eqidd	$⊢ z = v \to u = u$
35		eqidd	$⊢ z = v \to x = x$
36		id	$⊢ z = v \to z = v$
37	34 35 36	s3eqd	$⊢ z = v \to ⟨“ u x z ”⟩ = ⟨“ u x v ”⟩$
38	37	eleq1d	$⊢ z = v \to (⟨“ u x z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
39	33 38	rspc2va	$⊢ ((u \in A \land v \in B) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
40	26 27 28 39	syl21anc	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
41		simpllr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \neq u$
42	41	necomd	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \neq x$
43	42	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u \neq x$
44		simpr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \neq v$
45	44	necomd	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \neq x$
46	45	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to v \neq x$
47	1 2 3 4 25 10 24 17 21 40 43 46	ragncol	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to \neg (v \in (u L x) \lor u = x)$
48	1 4 3 10 24 17 21 47	ncolrot2	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to \neg (x \in (v L u) \lor v = u)$
49	1 3 4 10 17 21 24 17 48	tglineneq	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x L v \neq u L x$
50	49	necomd	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to u L x \neq x L v$
51	1 3 4 11 23 16 42 42 12 22 15	tglinethru	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to A = u L x$
52	51	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to A = u L x$
53	13	elin2d	$⊢ (φ \land x \in (A \cap B)) \to x \in B$
54	53	ad4antr	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to x \in B$
55	1 3 4 11 16 20 44 44 18 54 19	tglinethru	$⊢ (((((φ \land x \in (A \cap B)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to B = x L v$
56	55	adantl4r	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to B = x L v$
57	50 52 56	3netr4d	$⊢ ((((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \land v \in B) \land x \neq v) \to A \neq B$
58	7	adantr	$⊢ (φ \land x \in (A \cap B)) \to B \in ran L$
59	1 3 4 9 58 53	tglnpt2	$⊢ (φ \land x \in (A \cap B)) \to \exists v \in B x \neq v$
60	59	ad5ant12	$⊢ ((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \to \exists v \in B x \neq v$
61	57 60	r19.29a	$⊢ ((((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \land u \in A) \land x \neq u) \to A \neq B$
62	6	adantr	$⊢ (φ \land x \in (A \cap B)) \to A \in ran L$
63	1 3 4 9 62 14	tglnpt2	$⊢ (φ \land x \in (A \cap B)) \to \exists u \in A x \neq u$
64	63	adantr	$⊢ ((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \to \exists u \in A x \neq u$
65	61 64	r19.29a	$⊢ ((φ \land x \in (A \cap B)) \land \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)) \to A \neq B$
66	1 2 3 4 5 6 7	isperp	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \exists x \in (A \cap B) \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G))$
67	8 66	mpbid	$⊢ φ \to \exists x \in (A \cap B) \forall y \in A \forall z \in B ⟨“ y x z ”⟩ \in ∟_{𝒢} (G)$
68	65 67	r19.29a	$⊢ φ \to A \neq B$

Metamath Proof Explorer

Theorem perpneq

Proof