iscgra1

Description: A special version of iscgra where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
	iscgra1.m	$⊢ \underset{˙}{-} = dist (G)$
	iscgra1.1	$⊢ φ \to A \neq B$
	iscgra1.2	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
Assertion	iscgra1	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		iscgra1.m	$⊢ \underset{˙}{-} = dist (G)$
12		iscgra1.1	$⊢ φ \to A \neq B$
13		iscgra1.2	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
14	1 2 3 4 5 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists y \in P \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F))$
15	9	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to E \in P$
16	6	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to B \in P$
17	5	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to A \in P$
18	4	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to G \in 𝒢_{Tarski}$
19	8	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to D \in P$
20		simpllr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to y \in P$
21		simpr2	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to y K (E) D$
22	1 2 3 20 19 15 18 21	hlne2	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to D \neq E$
23	12	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to A \neq B$
24	23	necomd	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to B \neq A$
25	1 2 3 19 15 15 18 22	hlid	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to D K (E) D$
26		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
27	7	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to C \in P$
28		simplr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to x \in P$
29		simpr1	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩$
30	1 11 2 26 18 17 16 27 20 15 28 29	cgr3simp1	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to A \underset{˙}{-} B = y \underset{˙}{-} E$
31	30	eqcomd	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to y \underset{˙}{-} E = A \underset{˙}{-} B$
32	1 11 2 18 20 15 17 16 31	tgcgrcomlr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to E \underset{˙}{-} y = B \underset{˙}{-} A$
33	13	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
34	33	eqcomd	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to D \underset{˙}{-} E = A \underset{˙}{-} B$
35	1 11 2 18 19 15 17 16 34	tgcgrcomlr	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to E \underset{˙}{-} D = B \underset{˙}{-} A$
36	1 2 3 15 16 17 18 19 11 22 24 20 19 21 25 32 35	hlcgreulem	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to y = D$
37		simpr3	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to x K (E) F$
38	36 29 37	jca32	$⊢ (((φ \land y \in P) \land x \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)) \to (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))$
39		simprrl	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩$
40		simprl	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to y = D$
41	8	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to D \in P$
42	9	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to E \in P$
43	4	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to G \in 𝒢_{Tarski}$
44	1 11 2 4 5 6 8 9 13 12	tgcgrneq	$⊢ φ \to D \neq E$
45	44	ad3antrrr	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to D \neq E$
46	1 2 3 41 41 42 43 45	hlid	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to D K (E) D$
47	40 46	eqbrtrd	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to y K (E) D$
48		simprrr	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to x K (E) F$
49	39 47 48	3jca	$⊢ (((φ \land y \in P) \land x \in P) \land (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F)$
50	38 49	impbida	$⊢ ((φ \land y \in P) \land x \in P) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F) \leftrightarrow (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)))$
51	50	rexbidva	$⊢ (φ \land y \in P) \to (\exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F) \leftrightarrow \exists x \in P (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)))$
52		r19.42v	$⊢ \exists x \in P (y = D \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)) \leftrightarrow (y = D \land \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F))$
53	51 52	bitrdi	$⊢ (φ \land y \in P) \to (\exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F) \leftrightarrow (y = D \land \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)))$
54	53	rexbidva	$⊢ φ \to (\exists y \in P \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land y K (E) D \land x K (E) F) \leftrightarrow \exists y \in P (y = D \land \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)))$
55		id	$⊢ y = D \to y = D$
56		eqidd	$⊢ y = D \to E = E$
57		eqidd	$⊢ y = D \to x = x$
58	55 56 57	s3eqd	$⊢ y = D \to ⟨“ y E x ”⟩ = ⟨“ D E x ”⟩$
59	58	breq2d	$⊢ y = D \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩)$
60	59	anbi1d	$⊢ y = D \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$
61	60	rexbidv	$⊢ y = D \to (\exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F) \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$
62	61	ceqsrexv	$⊢ D \in P \to (\exists y \in P (y = D \land \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)) \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$
63	8 62	syl	$⊢ φ \to (\exists y \in P (y = D \land \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ y E x ”⟩ \land x K (E) F)) \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$
64	14 54 63	3bitrd	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E x ”⟩ \land x K (E) F))$

Metamath Proof Explorer

Theorem iscgra1

Proof