perpeqlem

	Ref	Expression
Hypotheses	perpeq.1	$⊢ P = {Base}_{G}$
	perpeq.2	$⊢ L = {Line}_{𝒢} (G)$
	perpeq.3	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	perpeq.4	$⊢ φ \to G \in 𝒢_{Tarski}$
	perpeq.5	$⊢ φ \to A \in ran L$
	perpeq.6	$⊢ φ \to H \in ran E$
	perpeq.7	$⊢ φ \to X \in A$
	perpeq.8	$⊢ φ \to A \subseteq H$
	perpeq.9	$⊢ φ \to Y \in H$
	perpeq.10	$⊢ φ \to Z \in H$
	perpeq.11	$⊢ φ \to (X L Y) ⟂_{𝒢} (G) A$
	perpeq.12	$⊢ φ \to (X L Z) ⟂_{𝒢} (G) A$
	perpeqlem.1	$⊢ φ \to Y {hp}_{𝒢} (G) (A) Z$
Assertion	perpeqlem	$⊢ φ \to X L Y = X L Z$

Proof

Step	Hyp	Ref	Expression
1		perpeq.1	$⊢ P = {Base}_{G}$
2		perpeq.2	$⊢ L = {Line}_{𝒢} (G)$
3		perpeq.3	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		perpeq.4	$⊢ φ \to G \in 𝒢_{Tarski}$
5		perpeq.5	$⊢ φ \to A \in ran L$
6		perpeq.6	$⊢ φ \to H \in ran E$
7		perpeq.7	$⊢ φ \to X \in A$
8		perpeq.8	$⊢ φ \to A \subseteq H$
9		perpeq.9	$⊢ φ \to Y \in H$
10		perpeq.10	$⊢ φ \to Z \in H$
11		perpeq.11	$⊢ φ \to (X L Y) ⟂_{𝒢} (G) A$
12		perpeq.12	$⊢ φ \to (X L Z) ⟂_{𝒢} (G) A$
13		perpeqlem.1	$⊢ φ \to Y {hp}_{𝒢} (G) (A) Z$
14		eqid	$⊢ Itv (G) = Itv (G)$
15	4	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to G \in 𝒢_{Tarski}$
16	1 2 14 4 5 7	tglnpt	$⊢ φ \to X \in P$
17	16	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \in P$
18	1 14 2 3 4 6 9	plngrnssp	$⊢ φ \to Y \in P$
19	18	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y \in P$
20	2 4 11	perpln1	$⊢ φ \to X L Y \in ran L$
21	1 14 2 4 16 18 20	tglnne	$⊢ φ \to X \neq Y$
22	21	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \neq Y$
23	2 4 12	perpln1	$⊢ φ \to X L Z \in ran L$
24	23	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X L Z \in ran L$
25	1 14 2 3 4 6 10	plngrnssp	$⊢ φ \to Z \in P$
26	1 14 2 4 16 25 23	tglnne	$⊢ φ \to X \neq Z$
27	26	necomd	$⊢ φ \to Z \neq X$
28	1 14 2 4 25 16 27	tglinerflx2	$⊢ φ \to X \in (Z L X)$
29	1 14 2 4 16 25 26	tglinecom	$⊢ φ \to X L Z = Z L X$
30	28 29	eleqtrrd	$⊢ φ \to X \in (X L Z)$
31	30	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \in (X L Z)$
32		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
33	25	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Z \in P$
34	5	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to A \in ran L$
35		simplr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to t \in (A ∖ (X L Y))$
36	35	eldifad	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to t \in A$
37	1 2 14 15 34 36	tglnpt	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to t \in P$
38		simpr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to t \neq X$
39	38	necomd	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \neq t$
40		eqid	$⊢ dist (G) = dist (G)$
41		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
42	21	necomd	$⊢ φ \to Y \neq X$
43	1 14 2 4 18 16 42	tglinerflx2	$⊢ φ \to X \in (Y L X)$
44	43	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \in (Y L X)$
45	11	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to (X L Y) ⟂_{𝒢} (G) A$
46	1 14 2 15 17 19 22	tglinecom	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X L Y = Y L X$
47	7	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \in A$
48	1 14 2 15 17 37 39 39 34 47 36	tglinethru	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to A = X L t$
49	45 46 48	3brtr3d	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to (Y L X) ⟂_{𝒢} (G) (X L t)$
50	1 40 14 2 15 19 17 44 37 49	perprag	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to ⟨“ Y X t ”⟩ \in ∟_{𝒢} (G)$
51	1 40 14 2 41 15 19 17 37 50	ragcom	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to ⟨“ t X Y ”⟩ \in ∟_{𝒢} (G)$
52	28	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X \in (Z L X)$
53	29 12	eqbrtrrd	$⊢ φ \to (Z L X) ⟂_{𝒢} (G) A$
54	53	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to (Z L X) ⟂_{𝒢} (G) A$
55	54 48	breqtrd	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to (Z L X) ⟂_{𝒢} (G) (X L t)$
56	1 40 14 2 15 33 17 52 37 55	perprag	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to ⟨“ Z X t ”⟩ \in ∟_{𝒢} (G)$
57	1 40 14 2 41 15 33 17 37 56	ragcom	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to ⟨“ t X Z ”⟩ \in ∟_{𝒢} (G)$
58	1 14 2 15 37 17 38 38 34 36 47	tglinethru	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to A = t L X$
59	58	fveq2d	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to {hp}_{𝒢} (G) (A) = {hp}_{𝒢} (G) (t L X)$
60	13	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y {hp}_{𝒢} (G) (A) Z$
61	59 60	breqdi	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y {hp}_{𝒢} (G) (t L X) Z$
62	1 2 15 17 37 19 33 39 51 57 61	ragraghl	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y {hl}_{𝒢} (G) (X) Z$
63	1 14 32 19 33 17 15 2 62	hlln	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y \in (Z L X)$
64	29	ad2antrr	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X L Z = Z L X$
65	63 64	eleqtrrd	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to Y \in (X L Z)$
66	1 14 2 15 17 19 22 22 24 31 65	tglinethru	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X L Z = X L Y$
67	66	eqcomd	$⊢ ((φ \land t \in (A ∖ (X L Y))) \land t \neq X) \to X L Y = X L Z$
68	1 40 14 2 4 20 5 11	perpneq	$⊢ φ \to X L Y \neq A$
69	68	necomd	$⊢ φ \to A \neq X L Y$
70	1 14 2 4 5 20 7 69	tglnpt4	$⊢ φ \to \exists t \in (A ∖ (X L Y)) t \neq X$
71	67 70	r19.29a	$⊢ φ \to X L Y = X L Z$

Metamath Proof Explorer

Theorem perpeqlem

Proof