trgcopy

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020)

	Ref	Expression
Hypotheses	trgcopy.p	$⊢ P = {Base}_{G}$
	trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
	trgcopy.i	$⊢ I = Itv (G)$
	trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
	trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
	trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	trgcopy.a	$⊢ φ \to A \in P$
	trgcopy.b	$⊢ φ \to B \in P$
	trgcopy.c	$⊢ φ \to C \in P$
	trgcopy.d	$⊢ φ \to D \in P$
	trgcopy.e	$⊢ φ \to E \in P$
	trgcopy.f	$⊢ φ \to F \in P$
	trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
	trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
Assertion	trgcopy	$⊢ φ \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$

Proof

Step	Hyp	Ref	Expression
1		trgcopy.p	$⊢ P = {Base}_{G}$
2		trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
3		trgcopy.i	$⊢ I = Itv (G)$
4		trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
5		trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
6		trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		trgcopy.a	$⊢ φ \to A \in P$
8		trgcopy.b	$⊢ φ \to B \in P$
9		trgcopy.c	$⊢ φ \to C \in P$
10		trgcopy.d	$⊢ φ \to D \in P$
11		trgcopy.e	$⊢ φ \to E \in P$
12		trgcopy.f	$⊢ φ \to F \in P$
13		trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
14		trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
15		trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
16		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
17	6	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to G \in 𝒢_{Tarski}$
18	17	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to G \in 𝒢_{Tarski}$
19	18	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to G \in 𝒢_{Tarski}$
20	19	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to G \in 𝒢_{Tarski}$
21	7	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \in P$
22	21	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to A \in P$
23	22	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to A \in P$
24	8	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to B \in P$
25	24	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to B \in P$
26	25	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to B \in P$
27	9	ad6antr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to C \in P$
28	27	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C \in P$
29	10	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to D \in P$
30	29	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to D \in P$
31	30	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to D \in P$
32	11	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to E \in P$
33	32	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to E \in P$
34	33	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to E \in P$
35		simprl	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f \in P$
36	15	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
37	36	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
38	1 4 3 6 8 9 7 13	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
39	38	ad4antr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to G {Dim}_{𝒢} \geq 2$
40	39	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to G {Dim}_{𝒢} \geq 2$
41	1 3 4 6 7 8 9 13	ncolne1	$⊢ φ \to A \neq B$
42	1 3 4 6 7 8 41	tgelrnln	$⊢ φ \to A L B \in ran L$
43	42	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A L B \in ran L$
44		simplr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \in (A L B)$
45	1 4 3 17 43 44	tglnpt	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \in P$
46	45	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to x \in P$
47	46	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to x \in P$
48	47	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \in P$
49		simplr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to y \in P$
50	49	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to y \in P$
51	50	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \in P$
52	44	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \in (A L B)$
53	41	ad7antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to A \neq B$
54	1 3 4 20 23 26 53	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to A L B = B L A$
55	52 54	eleqtrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \in (B L A)$
56		simp-6r	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (C L x) ⟂_{𝒢} (G) (A L B)$
57	4 20 56	perpln1	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C L x \in ran L$
58	43	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to A L B \in ran L$
59	1 2 3 4 20 57 58 56	perpcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (A L B) ⟂_{𝒢} (G) (C L x)$
60	1 4 3 6 8 9 7 13	ncolrot2	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
61		ioran	$⊢ \neg (C \in (A L B) \lor A = B) \leftrightarrow (\neg C \in (A L B) \land \neg A = B)$
62	60 61	sylib	$⊢ φ \to (\neg C \in (A L B) \land \neg A = B)$
63	62	simpld	$⊢ φ \to \neg C \in (A L B)$
64	63	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \neg C \in (A L B)$
65		nelne2	$⊢ (x \in (A L B) \land \neg C \in (A L B)) \to x \neq C$
66	44 64 65	syl2anc	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \neq C$
67	66	ad4antr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to x \neq C$
68	67	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \neq C$
69	68	necomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C \neq x$
70	1 3 4 20 28 48 69	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C L x = x L C$
71	59 54 70	3brtr3d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (B L A) ⟂_{𝒢} (G) (x L C)$
72	1 2 3 4 20 26 23 55 28 71	perprag	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ B x C ”⟩ \in ∟_{𝒢} (G)$
73	1 3 4 6 10 11 12 14	ncolne1	$⊢ φ \to D \neq E$
74	73	necomd	$⊢ φ \to E \neq D$
75	74	ad7antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to E \neq D$
76	73	ad4antr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to D \neq E$
77	76	neneqd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to \neg D = E$
78	44	orcd	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (x \in (A L B) \lor A = B)$
79	1 4 3 17 21 24 45 78	colrot2	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (B \in (x L A) \lor x = A)$
80	1 4 3 17 45 21 24 79	colcom	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (B \in (A L x) \lor A = x)$
81	80	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (B \in (A L x) \lor A = x)$
82		simpr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩$
83	1 4 3 18 22 25 46 16 30 33 49 81 82	lnxfr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (E \in (D L y) \lor D = y)$
84	1 4 3 18 30 49 33 83	colrot2	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (y \in (E L D) \lor E = D)$
85	1 4 3 18 33 30 49 84	colcom	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (y \in (D L E) \lor D = E)$
86	85	orcomd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (D = E \lor y \in (D L E))$
87	86	ord	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (\neg D = E \to y \in (D L E))$
88	77 87	mpd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to y \in (D L E)$
89	88	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \in (D L E)$
90	1 3 4 20 34 31 51 75 89	lncom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \in (E L D)$
91		simprrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \underset{˙}{-} f = x \underset{˙}{-} C$
92	91	eqcomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \underset{˙}{-} C = y \underset{˙}{-} f$
93	1 2 3 20 48 28 51 35 92 68	tgcgrneq	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \neq f$
94	1 3 4 20 51 35 93	tgelrnln	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y L f \in ran L$
95	1 3 4 20 34 31 75	tgelrnln	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to E L D \in ran L$
96		simpllr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to q \in P$
97		simplr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to q \in P$
98		simprl	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to (D L E) ⟂_{𝒢} (G) (q L y)$
99	4 19 98	perpln2	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to q L y \in ran L$
100	1 3 4 19 97 50 99	tglnne	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to q \neq y$
101	100	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to q \neq y$
102	101	necomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y \neq q$
103	1 3 4 20 51 96 102	tgelrnln	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y L q \in ran L$
104	98	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (D L E) ⟂_{𝒢} (G) (q L y)$
105	1 3 4 20 34 31 75	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to E L D = D L E$
106	1 3 4 20 51 96 102	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to y L q = q L y$
107	104 105 106	3brtr4d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (E L D) ⟂_{𝒢} (G) (y L q)$
108	1 2 3 4 20 95 103 107	perpcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (y L q) ⟂_{𝒢} (G) (E L D)$
109		simprrl	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f K (y) q$
110	1 3 5 35 96 51 20 4 109	hlln	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f \in (q L y)$
111	1 3 4 20 51 96 35 102 110	lncom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f \in (y L q)$
112	111	orcd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (f \in (y L q) \lor y = q)$
113	1 2 3 4 20 51 96 35 108 112 93	colperp	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (y L f) ⟂_{𝒢} (G) (E L D)$
114	1 2 3 4 20 94 95 113	perpcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (E L D) ⟂_{𝒢} (G) (y L f)$
115	1 2 3 4 20 34 31 90 35 114	perprag	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ E y f ”⟩ \in ∟_{𝒢} (G)$
116	82	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩$
117	1 2 3 16 20 23 26 48 31 34 51 116	cgr3simp2	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to B \underset{˙}{-} x = E \underset{˙}{-} y$
118	1 2 3 20 40 26 48 28 34 51 35 72 115 117 92	hypcgr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to B \underset{˙}{-} C = E \underset{˙}{-} f$
119		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
120	54 71	eqbrtrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (A L B) ⟂_{𝒢} (G) (x L C)$
121	1 2 3 4 20 23 26 52 28 120	perprag	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ A x C ”⟩ \in ∟_{𝒢} (G)$
122	1 2 3 4 119 20 23 48 28 121	ragcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ C x A ”⟩ \in ∟_{𝒢} (G)$
123	105 114	eqbrtrrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (D L E) ⟂_{𝒢} (G) (y L f)$
124	1 2 3 4 20 31 34 89 35 123	perprag	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ D y f ”⟩ \in ∟_{𝒢} (G)$
125	1 2 3 4 119 20 31 51 35 124	ragcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ f y D ”⟩ \in ∟_{𝒢} (G)$
126	1 2 3 20 48 28 51 35 92	tgcgrcomlr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C \underset{˙}{-} x = f \underset{˙}{-} y$
127	1 2 3 16 20 23 26 48 31 34 51 116	cgr3simp3	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to x \underset{˙}{-} A = y \underset{˙}{-} D$
128	1 2 3 20 40 28 48 23 35 51 31 122 125 126 127	hypcgr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to C \underset{˙}{-} A = f \underset{˙}{-} D$
129	1 2 16 20 23 26 28 31 34 35 37 118 128	trgcgr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩$
130	1 3 4 6 10 11 73	tgelrnln	$⊢ φ \to D L E \in ran L$
131	130	ad4antr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to D L E \in ran L$
132	131	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to D L E \in ran L$
133		simpl	$⊢ (w = k \land v = l) \to w = k$
134	133	eleq1d	$⊢ (w = k \land v = l) \to (w \in (P ∖ (D L E)) \leftrightarrow k \in (P ∖ (D L E)))$
135		simpr	$⊢ (w = k \land v = l) \to v = l$
136	135	eleq1d	$⊢ (w = k \land v = l) \to (v \in (P ∖ (D L E)) \leftrightarrow l \in (P ∖ (D L E)))$
137	134 136	anbi12d	$⊢ (w = k \land v = l) \to ((w \in (P ∖ (D L E)) \land v \in (P ∖ (D L E))) \leftrightarrow (k \in (P ∖ (D L E)) \land l \in (P ∖ (D L E))))$
138		simpr	$⊢ ((w = k \land v = l) \land z = j) \to z = j$
139		simpll	$⊢ ((w = k \land v = l) \land z = j) \to w = k$
140		simplr	$⊢ ((w = k \land v = l) \land z = j) \to v = l$
141	139 140	oveq12d	$⊢ ((w = k \land v = l) \land z = j) \to w I v = k I l$
142	138 141	eleq12d	$⊢ ((w = k \land v = l) \land z = j) \to (z \in (w I v) \leftrightarrow j \in (k I l))$
143	142	cbvrexdva	$⊢ (w = k \land v = l) \to (\exists z \in (D L E) z \in (w I v) \leftrightarrow \exists j \in (D L E) j \in (k I l))$
144	137 143	anbi12d	$⊢ (w = k \land v = l) \to (((w \in (P ∖ (D L E)) \land v \in (P ∖ (D L E))) \land \exists z \in (D L E) z \in (w I v)) \leftrightarrow ((k \in (P ∖ (D L E)) \land l \in (P ∖ (D L E))) \land \exists j \in (D L E) j \in (k I l)))$
145	144	cbvopabv	$⊢ \{⟨w, v⟩ \| ((w \in (P ∖ (D L E)) \land v \in (P ∖ (D L E))) \land \exists z \in (D L E) z \in (w I v))\} = \{⟨k, l⟩ \| ((k \in (P ∖ (D L E)) \land l \in (P ∖ (D L E))) \land \exists j \in (D L E) j \in (k I l))\}$
146	20	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to G \in 𝒢_{Tarski}$
147	28	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to C \in P$
148	26	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to B \in P$
149	23	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to A \in P$
150	31	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to D \in P$
151	34	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to E \in P$
152	35	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to f \in P$
153	74	ad8antr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to E \neq D$
154		simpr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to f \in (D L E)$
155	1 3 4 146 151 150 152 153 154	lncom	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to f \in (E L D)$
156	155	orcd	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to (f \in (E L D) \lor E = D)$
157	1 4 3 146 151 150 152 156	colrot1	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to (E \in (D L f) \lor D = f)$
158	129	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩$
159	1 2 3 16 146 149 148 147 150 151 152 158	trgcgrcom	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to ⟨“ D E f ”⟩ \sim_{𝒢} (G) ⟨“ A B C ”⟩$
160	1 4 3 146 150 151 152 16 149 148 147 157 159	lnxfr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to (B \in (A L C) \lor A = C)$
161	1 4 3 146 149 147 148 160	colrot1	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to (A \in (C L B) \lor C = B)$
162	1 4 3 146 147 148 149 161	colcom	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to (A \in (B L C) \lor B = C)$
163	13	ad8antr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \land f \in (D L E)) \to \neg (A \in (B L C) \lor B = C)$
164	162 163	pm2.65da	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to \neg f \in (D L E)$
165	1 3 4 20 132 51 145 5 89 35 96 164 109	hphl	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f {hp}_{𝒢} (G) (D L E) q$
166	12	ad4antr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to F \in P$
167	166	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to F \in P$
168	167	adantr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to F \in P$
169		simplrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to q {hp}_{𝒢} (G) (D L E) F$
170	1 3 4 20 132 35 145 96 165 168 169	hpgtr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to f {hp}_{𝒢} (G) (D L E) F$
171	129 170	jca	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \land (f \in P \land (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C))) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
172	1 3 5 50 47 27 19 97 2 100 67	hlcgrex	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to \exists f \in P (f K (y) q \land y \underset{˙}{-} f = x \underset{˙}{-} C)$
173	171 172	reximddv	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \land q \in P) \land ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
174	1 4 3 6 11 12 10 14	ncolrot2	$⊢ φ \to \neg (F \in (D L E) \lor D = E)$
175		ioran	$⊢ \neg (F \in (D L E) \lor D = E) \leftrightarrow (\neg F \in (D L E) \land \neg D = E)$
176	174 175	sylib	$⊢ φ \to (\neg F \in (D L E) \land \neg D = E)$
177	176	simpld	$⊢ φ \to \neg F \in (D L E)$
178	177	ad4antr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to \neg F \in (D L E)$
179	1 2 3 4 18 39 131 145 88 166 178	lnperpex	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to \exists q \in P ((D L E) ⟂_{𝒢} (G) (q L y) \land q {hp}_{𝒢} (G) (D L E) F)$
180	173 179	r19.29a	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land y \in P) \land ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
181	1 4 3 17 21 24 45 16 29 32 2 80 36	lnext	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \exists y \in P ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩$
182	180 181	r19.29a	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
183	1 2 3 4 6 42 9 63	footex	$⊢ φ \to \exists x \in (A L B) (C L x) ⟂_{𝒢} (G) (A L B)$
184	182 183	r19.29a	$⊢ φ \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$

Metamath Proof Explorer

Theorem trgcopy

Proof