iscgrag

Description: Ray normalization: an angle congruence yields two points on the target rays carrying a full triangle congruence, together with the two arm lengths. This is the forward direction of iscgra (Schwabhauser 11.3) repackaged -- nothing is constructed; the distances are read off the cgrG with cgr3simp1 and cgr3simp2 . No non-degeneracy hypothesis is needed or wanted: cgrA carries vertex distinctness intrinsically ( cgrane1 through cgrane4 ), and an extra hypothesis would obstruct the degenerate branches. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		iscgrag.p	$⊢ P = {Base}_{G}$
2		iscgrag.i	$⊢ I = Itv (G)$
3		iscgrag.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgrag.m	$⊢ \underset{˙}{-} = dist (G)$
5		iscgrag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		iscgrag.a	$⊢ φ \to A \in P$
7		iscgrag.b	$⊢ φ \to B \in P$
8		iscgrag.c	$⊢ φ \to C \in P$
9		iscgrag.d	$⊢ φ \to D \in P$
10		iscgrag.e	$⊢ φ \to E \in P$
11		iscgrag.f	$⊢ φ \to F \in P$
12		iscgrag.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
13		simpr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)$
14		simpll	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (φ \land x \in P)$
15	14	simpld	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to φ$
16	15 5	syl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to G \in 𝒢_{Tarski}$
17	15 6	syl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \in P$
18	15 7	syl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \in P$
19	14	simprd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \in P$
20	15 10	syl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \in P$
21		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
22	15 8	syl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \in P$
23		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y \in P$
24	13	simp1d	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
25	1 4 2 21 16 17 18 22 19 20 23 24	cgr3simp1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \underset{˙}{-} B = x \underset{˙}{-} E$
26	1 4 2 16 17 18 19 20 25	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} A = E \underset{˙}{-} x$
27	26	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \underset{˙}{-} x = B \underset{˙}{-} A$
28	1 4 2 21 16 17 18 22 19 20 23 24	cgr3simp2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} C = E \underset{˙}{-} y$
29	28	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \underset{˙}{-} y = B \underset{˙}{-} C$
30	27 29	jca	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C)$
31	13 30	jca	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \land (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
32	31	ex	$⊢ ((φ \land x \in P) \land y \in P) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \land (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C)))$
33	32	reximdva	$⊢ (φ \land x \in P) \to (\exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \to \exists y \in P ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \land (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C)))$
34	33	imp	$⊢ ((φ \land x \in P) \land \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to \exists y \in P ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \land (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
35	1 2 3 5 6 7 8 9 10 11	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
36	12 35	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)$
37	34 36	reximddv3	$⊢ φ \to \exists x \in P \exists y \in P ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \land (E \underset{˙}{-} x = B \underset{˙}{-} A \land E \underset{˙}{-} y = B \underset{˙}{-} C))$

Metamath Proof Explorer

Theorem iscgrag

Proof