cgrgptxfr

Description: Transfer a segment point across a triangle congruence: given <" A B C "> cgrG <" X E Z "> and J between A and C , the corresponding point on ( X I Z ) exists, with its betweenness, its two distances and the sub-triangle congruence. GeoCoq reaches this through l4__6 and cong2__conga__cong ; here cgrg3col4 (Schwabhauser 11.28) constructs the point with every pairwise distance and tgbtwnxfr -- which *is* l4__6 -- supplies the image betweenness. The A = C case takes cgrg3col4 's right disjunct, since tgellng needs A =/= C and cgrA does not supply it. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	cgrgptxfr.p	$⊢ P = {Base}_{G}$
	cgrgptxfr.i	$⊢ I = Itv (G)$
	cgrgptxfr.m	$⊢ \underset{˙}{-} = dist (G)$
	cgrgptxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgrgptxfr.a	$⊢ φ \to A \in P$
	cgrgptxfr.b	$⊢ φ \to B \in P$
	cgrgptxfr.c	$⊢ φ \to C \in P$
	cgrgptxfr.x	$⊢ φ \to X \in P$
	cgrgptxfr.e	$⊢ φ \to E \in P$
	cgrgptxfr.z	$⊢ φ \to Z \in P$
	cgrgptxfr.j	$⊢ φ \to J \in P$
	cgrgptxfr.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Z ”⟩$
	cgrgptxfr.2	$⊢ φ \to J \in (A I C)$
Assertion	cgrgptxfr	$⊢ φ \to \exists y \in P ((y \in (X I Z) \land ⟨“ A B J ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩) \land (A \underset{˙}{-} J = X \underset{˙}{-} y \land J \underset{˙}{-} C = y \underset{˙}{-} Z))$

Proof

Step	Hyp	Ref	Expression
1		cgrgptxfr.p	$⊢ P = {Base}_{G}$
2		cgrgptxfr.i	$⊢ I = Itv (G)$
3		cgrgptxfr.m	$⊢ \underset{˙}{-} = dist (G)$
4		cgrgptxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgrgptxfr.a	$⊢ φ \to A \in P$
6		cgrgptxfr.b	$⊢ φ \to B \in P$
7		cgrgptxfr.c	$⊢ φ \to C \in P$
8		cgrgptxfr.x	$⊢ φ \to X \in P$
9		cgrgptxfr.e	$⊢ φ \to E \in P$
10		cgrgptxfr.z	$⊢ φ \to Z \in P$
11		cgrgptxfr.j	$⊢ φ \to J \in P$
12		cgrgptxfr.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Z ”⟩$
13		cgrgptxfr.2	$⊢ φ \to J \in (A I C)$
14		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
15		simpll	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to φ$
16	15 4	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to G \in 𝒢_{Tarski}$
17	15 5	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to A \in P$
18	15 11	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to J \in P$
19	15 7	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to C \in P$
20	15 8	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to X \in P$
21		simplr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to y \in P$
22	15 10	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to Z \in P$
23		simpr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩$
24	15 6	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to B \in P$
25	15 9	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to E \in P$
26	1 3 2 14 16 17 24 19 18 20 25 22 21	tgcgr4	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to (⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Z ”⟩ \land (A \underset{˙}{-} J = X \underset{˙}{-} y \land B \underset{˙}{-} J = E \underset{˙}{-} y \land C \underset{˙}{-} J = Z \underset{˙}{-} y)))$
27	23 26	mpbid	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Z ”⟩ \land (A \underset{˙}{-} J = X \underset{˙}{-} y \land B \underset{˙}{-} J = E \underset{˙}{-} y \land C \underset{˙}{-} J = Z \underset{˙}{-} y))$
28	27	simprd	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to (A \underset{˙}{-} J = X \underset{˙}{-} y \land B \underset{˙}{-} J = E \underset{˙}{-} y \land C \underset{˙}{-} J = Z \underset{˙}{-} y)$
29	28	simp1d	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to A \underset{˙}{-} J = X \underset{˙}{-} y$
30	28	simp3d	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to C \underset{˙}{-} J = Z \underset{˙}{-} y$
31	1 3 2 16 19 18 22 21 30	tgcgrcomlr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to J \underset{˙}{-} C = y \underset{˙}{-} Z$
32	15 12	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Z ”⟩$
33	1 3 2 14 16 17 24 19 20 25 22 32	cgr3simp3	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to C \underset{˙}{-} A = Z \underset{˙}{-} X$
34	1 3 14 16 17 18 19 20 21 22 29 31 33	trgcgr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to ⟨“ A J C ”⟩ \sim_{𝒢} (G) ⟨“ X y Z ”⟩$
35	15 13	syl	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to J \in (A I C)$
36	1 3 2 14 16 17 18 19 20 21 22 34 35	tgbtwnxfr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to y \in (X I Z)$
37	1 3 2 14 16 17 24 19 20 25 22 32	cgr3simp1	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to A \underset{˙}{-} B = X \underset{˙}{-} E$
38	28	simp2d	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to B \underset{˙}{-} J = E \underset{˙}{-} y$
39	1 3 2 16 17 18 20 21 29	tgcgrcomlr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to J \underset{˙}{-} A = y \underset{˙}{-} X$
40	1 3 14 16 17 24 18 20 25 21 37 38 39	trgcgr	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to ⟨“ A B J ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩$
41	36 40	jca	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to (y \in (X I Z) \land ⟨“ A B J ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩)$
42	29 31	jca	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to (A \underset{˙}{-} J = X \underset{˙}{-} y \land J \underset{˙}{-} C = y \underset{˙}{-} Z)$
43	41 42	jca	$⊢ ((φ \land y \in P) \land ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩) \to ((y \in (X I Z) \land ⟨“ A B J ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩) \land (A \underset{˙}{-} J = X \underset{˙}{-} y \land J \underset{˙}{-} C = y \underset{˙}{-} Z))$
44		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
45		simpr	$⊢ (φ \land A = C) \to A = C$
46	45	olcd	$⊢ (φ \land A = C) \to (J \in (A {Line}_{𝒢} (G) C) \lor A = C)$
47		simpl	$⊢ (φ \land A \neq C) \to φ$
48	47 13	syl	$⊢ (φ \land A \neq C) \to J \in (A I C)$
49	48	3mix1d	$⊢ (φ \land A \neq C) \to (J \in (A I C) \lor A \in (J I C) \lor C \in (A I J))$
50	47 4	syl	$⊢ (φ \land A \neq C) \to G \in 𝒢_{Tarski}$
51	47 5	syl	$⊢ (φ \land A \neq C) \to A \in P$
52	47 7	syl	$⊢ (φ \land A \neq C) \to C \in P$
53		simpr	$⊢ (φ \land A \neq C) \to A \neq C$
54	47 11	syl	$⊢ (φ \land A \neq C) \to J \in P$
55	1 44 2 50 51 52 53 54	tgellng	$⊢ (φ \land A \neq C) \to (J \in (A {Line}_{𝒢} (G) C) \leftrightarrow (J \in (A I C) \lor A \in (J I C) \lor C \in (A I J)))$
56	49 55	mpbird	$⊢ (φ \land A \neq C) \to J \in (A {Line}_{𝒢} (G) C)$
57	56	orcd	$⊢ (φ \land A \neq C) \to (J \in (A {Line}_{𝒢} (G) C) \lor A = C)$
58	46 57	pm2.61dane	$⊢ φ \to (J \in (A {Line}_{𝒢} (G) C) \lor A = C)$
59	1 4 5 6 7 8 9 10 44 11 12 58	cgrg3col4	$⊢ φ \to \exists y \in P ⟨“ A B C J ”⟩ \sim_{𝒢} (G) ⟨“ X E Z y ”⟩$
60	43 59	reximddv3	$⊢ φ \to \exists y \in P ((y \in (X I Z) \land ⟨“ A B J ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩) \land (A \underset{˙}{-} J = X \underset{˙}{-} y \land J \underset{˙}{-} C = y \underset{˙}{-} Z))$

Metamath Proof Explorer

Theorem cgrgptxfr

Proof