tgcgrxfr

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

	Ref	Expression
Hypotheses	tgcgrxfr.p	$⊢ P = {Base}_{G}$
	tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
	tgcgrxfr.i	$⊢ I = Itv (G)$
	tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgcgrxfr.a	$⊢ φ \to A \in P$
	tgcgrxfr.b	$⊢ φ \to B \in P$
	tgcgrxfr.c	$⊢ φ \to C \in P$
	tgcgrxfr.d	$⊢ φ \to D \in P$
	tgcgrxfr.f	$⊢ φ \to F \in P$
	tgcgrxfr.1	$⊢ φ \to B \in (A I C)$
	tgcgrxfr.2	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$
Assertion	tgcgrxfr	$⊢ φ \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		tgcgrxfr.p	$⊢ P = {Base}_{G}$
2		tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgcgrxfr.i	$⊢ I = Itv (G)$
4		tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
5		tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgcgrxfr.a	$⊢ φ \to A \in P$
7		tgcgrxfr.b	$⊢ φ \to B \in P$
8		tgcgrxfr.c	$⊢ φ \to C \in P$
9		tgcgrxfr.d	$⊢ φ \to D \in P$
10		tgcgrxfr.f	$⊢ φ \to F \in P$
11		tgcgrxfr.1	$⊢ φ \to B \in (A I C)$
12		tgcgrxfr.2	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$
13	6	adantr	$⊢ (φ \land \|P\| = 1) \to A \in P$
14	5	adantr	$⊢ (φ \land \|P\| = 1) \to G \in 𝒢_{Tarski}$
15	9	adantr	$⊢ (φ \land \|P\| = 1) \to D \in P$
16	10	adantr	$⊢ (φ \land \|P\| = 1) \to F \in P$
17		simpr	$⊢ (φ \land \|P\| = 1) \to \|P\| = 1$
18	1 2 3 14 13 15 16 17	tgldim0itv	$⊢ (φ \land \|P\| = 1) \to A \in (D I F)$
19	7	adantr	$⊢ (φ \land \|P\| = 1) \to B \in P$
20	8	adantr	$⊢ (φ \land \|P\| = 1) \to C \in P$
21	1 2 3 14 13 19 15 17 13	tgldim0cgr	$⊢ (φ \land \|P\| = 1) \to A \underset{˙}{-} B = D \underset{˙}{-} A$
22	1 2 3 14 19 20 13 17 16	tgldim0cgr	$⊢ (φ \land \|P\| = 1) \to B \underset{˙}{-} C = A \underset{˙}{-} F$
23	1 2 3 14 20 13 16 17 15	tgldim0cgr	$⊢ (φ \land \|P\| = 1) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
24	1 2 4 14 13 19 20 15 13 16 21 22 23	trgcgr	$⊢ (φ \land \|P\| = 1) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D A F ”⟩$
25		eleq1	$⊢ e = A \to (e \in (D I F) \leftrightarrow A \in (D I F))$
26		s3eq2	$⊢ e = A \to ⟨“ D e F ”⟩ = ⟨“ D A F ”⟩$
27	26	breq2d	$⊢ e = A \to (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D A F ”⟩)$
28	25 27	anbi12d	$⊢ e = A \to ((e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩) \leftrightarrow (A \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D A F ”⟩))$
29	28	rspcev	$⊢ (A \in P \land (A \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D A F ”⟩)) \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
30	13 18 24 29	syl12anc	$⊢ (φ \land \|P\| = 1) \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
31	5	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to G \in 𝒢_{Tarski}$
32		simplr	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to g \in P$
33	9	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to D \in P$
34	6	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to A \in P$
35	7	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to B \in P$
36	1 2 3 31 32 33 34 35	axtgsegcon	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to \exists e \in P (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)$
37	5	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
38	32	ad2antrr	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to g \in P$
39	38	ad2antrr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to g \in P$
40	9	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in P$
41		simplr	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to e \in P$
42	41	ad2antrr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \in P$
43		simplr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \in P$
44		simpllr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)$
45	44	simpld	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in (g I e)$
46		simprl	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \in (g I f)$
47	1 2 3 37 39 40 42 43 45 46	tgbtwnexch3	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \in (D I f)$
48	6	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \in P$
49	8	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to C \in P$
50	10	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to F \in P$
51		simp-5r	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to (D \in (F I g) \land D \neq g)$
52	51	simprd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \neq g$
53	52	necomd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to g \neq D$
54	1 2 3 37 39 40 42 43 45 46	tgbtwnexch	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in (g I f)$
55	51	simpld	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in (F I g)$
56	1 2 3 37 50 40 39 55	tgbtwncom	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in (g I F)$
57	7	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \in P$
58	11	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \in (A I C)$
59	44	simprd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \underset{˙}{-} e = A \underset{˙}{-} B$
60		simprr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \underset{˙}{-} f = B \underset{˙}{-} C$
61	1 2 3 37 40 42 43 48 57 49 47 58 59 60	tgcgrextend	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \underset{˙}{-} f = A \underset{˙}{-} C$
62	12	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
63	62	eqcomd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \underset{˙}{-} F = A \underset{˙}{-} C$
64	1 2 3 37 40 48 49 39 43 50 53 54 56 61 63	tgsegconeq	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to f = F$
65	64	oveq2d	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to D I f = D I F$
66	47 65	eleqtrd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \in (D I F)$
67	59	eqcomd	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \underset{˙}{-} B = D \underset{˙}{-} e$
68	64	oveq2d	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to e \underset{˙}{-} f = e \underset{˙}{-} F$
69	60 68	eqtr3d	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \underset{˙}{-} C = e \underset{˙}{-} F$
70	1 2 3 5 6 8 9 10 12	tgcgrcomlr	$⊢ φ \to C \underset{˙}{-} A = F \underset{˙}{-} D$
71	70	ad7antr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
72	1 2 4 37 48 57 49 40 42 50 67 69 71	trgcgr	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩$
73	66 72	jca	$⊢ (((((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \land f \in P) \land (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)) \to (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
74	31	ad2antrr	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to G \in 𝒢_{Tarski}$
75	35	ad2antrr	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to B \in P$
76	8	ad5antr	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to C \in P$
77	1 2 3 74 38 41 75 76	axtgsegcon	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to \exists f \in P (e \in (g I f) \land e \underset{˙}{-} f = B \underset{˙}{-} C)$
78	73 77	r19.29a	$⊢ (((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \land (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B)) \to (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
79	78	ex	$⊢ ((((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \land e \in P) \to ((D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B) \to (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩))$
80	79	reximdva	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to (\exists e \in P (D \in (g I e) \land D \underset{˙}{-} e = A \underset{˙}{-} B) \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩))$
81	36 80	mpd	$⊢ (((φ \land 2 \leq \|P\|) \land g \in P) \land (D \in (F I g) \land D \neq g)) \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
82	5	adantr	$⊢ (φ \land 2 \leq \|P\|) \to G \in 𝒢_{Tarski}$
83	10	adantr	$⊢ (φ \land 2 \leq \|P\|) \to F \in P$
84	9	adantr	$⊢ (φ \land 2 \leq \|P\|) \to D \in P$
85		simpr	$⊢ (φ \land 2 \leq \|P\|) \to 2 \leq \|P\|$
86	1 2 3 82 83 84 85	tgbtwndiff	$⊢ (φ \land 2 \leq \|P\|) \to \exists g \in P (D \in (F I g) \land D \neq g)$
87	81 86	r19.29a	$⊢ (φ \land 2 \leq \|P\|) \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
88	1 6	tgldimor	$⊢ φ \to (\|P\| = 1 \lor 2 \leq \|P\|)$
89	30 87 88	mpjaodan	$⊢ φ \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$

Metamath Proof Explorer

Theorem tgcgrxfr

Proof