ragcgra

Description: Right angles are congruent with each other. Theorem 11.16 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	ragcgra.p	$⊢ P = {Base}_{G}$
	ragcgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ragcgra.x	$⊢ φ \to X \in P$
	ragcgra.y	$⊢ φ \to Y \in P$
	ragcgra.z	$⊢ φ \to Z \in P$
	ragcgra.a	$⊢ φ \to A \in P$
	ragcgra.b	$⊢ φ \to B \in P$
	ragcgra.c	$⊢ φ \to C \in P$
	ragcgra.1	$⊢ φ \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
	ragcgra.2	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	ragcgra.3	$⊢ φ \to A \neq B$
	ragcgra.4	$⊢ φ \to B \neq C$
	ragcgra.5	$⊢ φ \to X \neq Y$
	ragcgra.6	$⊢ φ \to Y \neq Z$
Assertion	ragcgra	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$

Proof

Step	Hyp	Ref	Expression
1		ragcgra.p	$⊢ P = {Base}_{G}$
2		ragcgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
3		ragcgra.x	$⊢ φ \to X \in P$
4		ragcgra.y	$⊢ φ \to Y \in P$
5		ragcgra.z	$⊢ φ \to Z \in P$
6		ragcgra.a	$⊢ φ \to A \in P$
7		ragcgra.b	$⊢ φ \to B \in P$
8		ragcgra.c	$⊢ φ \to C \in P$
9		ragcgra.1	$⊢ φ \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
10		ragcgra.2	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
11		ragcgra.3	$⊢ φ \to A \neq B$
12		ragcgra.4	$⊢ φ \to B \neq C$
13		ragcgra.5	$⊢ φ \to X \neq Y$
14		ragcgra.6	$⊢ φ \to Y \neq Z$
15		eqid	$⊢ Itv (G) = Itv (G)$
16		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
17	2	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to G \in 𝒢_{Tarski}$
18	3	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to X \in P$
19	4	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Y \in P$
20	5	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Z \in P$
21	6	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to A \in P$
22	7	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to B \in P$
23	8	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to C \in P$
24		simp-6r	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to a \in P$
25		simpllr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to c \in P$
26		eqid	$⊢ dist (G) = dist (G)$
27		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
28		simp-4r	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to B dist (G) a = Y dist (G) X$
29	28	eqcomd	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Y dist (G) X = B dist (G) a$
30	1 26 15 17 19 18 22 24 29	tgcgrcomlr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to X dist (G) Y = a dist (G) B$
31		simpr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to B dist (G) c = Y dist (G) Z$
32	31	eqcomd	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Y dist (G) Z = B dist (G) c$
33		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
34		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
35	12	necomd	$⊢ φ \to C \neq B$
36	1 26 15 33 34 2 6 7 8 10 11 35	ragncol	$⊢ φ \to \neg (C \in (A {Line}_{𝒢} (G) B) \lor A = B)$
37	1 33 15 2 6 7 8 36	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
38	37	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to G {Dim}_{𝒢} \geq 2$
39	9	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
40	10	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
41	1 26 15 33 34 17 21 22 23 40	ragcom	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ C B A ”⟩ \in ∟_{𝒢} (G)$
42	35	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to C \neq B$
43	14	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Y \neq Z$
44	1 26 15 17 19 20 22 25 32 43	tgcgrneq	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to B \neq c$
45		simplr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to c {hl}_{𝒢} (G) (B) C$
46	1 15 16 25 23 22 17 33 45	hlln	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to c \in (C {Line}_{𝒢} (G) B)$
47	1 15 33 17 22 25 23 44 46 42	lnrot1	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to C \in (B {Line}_{𝒢} (G) c)$
48	47	orcd	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to (C \in (B {Line}_{𝒢} (G) c) \lor B = c)$
49	1 26 15 33 34 17 23 22 21 25 41 42 48	ragcol	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ c B A ”⟩ \in ∟_{𝒢} (G)$
50	1 26 15 33 34 17 25 22 21 49	ragcom	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ A B c ”⟩ \in ∟_{𝒢} (G)$
51	11	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to A \neq B$
52	13	necomd	$⊢ φ \to Y \neq X$
53	52	ad6antr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Y \neq X$
54	1 26 15 17 19 18 22 24 29 53	tgcgrneq	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to B \neq a$
55		simp-5r	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to a {hl}_{𝒢} (G) (B) A$
56	1 15 16 24 21 22 17 33 55	hlln	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to a \in (A {Line}_{𝒢} (G) B)$
57	1 15 33 17 22 24 21 54 56 51	lnrot1	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to A \in (B {Line}_{𝒢} (G) a)$
58	57	orcd	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to (A \in (B {Line}_{𝒢} (G) a) \lor B = a)$
59	1 26 15 33 34 17 21 22 25 24 50 51 58	ragcol	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ a B c ”⟩ \in ∟_{𝒢} (G)$
60	1 26 15 17 38 18 19 20 24 22 25 39 59 30 32	hypcgr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to X dist (G) Z = a dist (G) c$
61	1 26 15 17 18 20 24 25 60	tgcgrcomlr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to Z dist (G) X = c dist (G) a$
62	1 26 27 17 18 19 20 24 22 25 30 32 61	trgcgr	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩$
63	1 15 16 17 18 19 20 21 22 23 24 25 62 55 45	iscgrad	$⊢ ((((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land c {hl}_{𝒢} (G) (B) C) \land B dist (G) c = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
64	63	anasss	$⊢ (((((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \land c \in P) \land (c {hl}_{𝒢} (G) (B) C \land B dist (G) c = Y dist (G) Z)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
65	1 15 16 7 4 5 2 8 26 35 14	hlcgrex	$⊢ φ \to \exists c \in P (c {hl}_{𝒢} (G) (B) C \land B dist (G) c = Y dist (G) Z)$
66	65	ad3antrrr	$⊢ (((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \to \exists c \in P (c {hl}_{𝒢} (G) (B) C \land B dist (G) c = Y dist (G) Z)$
67	64 66	r19.29a	$⊢ (((φ \land a \in P) \land a {hl}_{𝒢} (G) (B) A) \land B dist (G) a = Y dist (G) X) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
68	67	anasss	$⊢ ((φ \land a \in P) \land (a {hl}_{𝒢} (G) (B) A \land B dist (G) a = Y dist (G) X)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
69	1 15 16 7 4 3 2 6 26 11 52	hlcgrex	$⊢ φ \to \exists a \in P (a {hl}_{𝒢} (G) (B) A \land B dist (G) a = Y dist (G) X)$
70	68 69	r19.29a	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$

Metamath Proof Explorer

Theorem ragcgra

Proof