cgrarag

Description: Any angle <" A B C "> congruent with a right angle <" X Y Z "> is a right angle. Theorem 11.17 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-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)$
	cgrarag.1	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
Assertion	cgrarag	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$

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		cgrarag.1	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
11		eqid	$⊢ dist (G) = dist (G)$
12		eqid	$⊢ Itv (G) = Itv (G)$
13		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
14		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
15	2	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to G \in 𝒢_{Tarski}$
16		simp-5r	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to a \in P$
17	7	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to B \in P$
18	8	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to C \in P$
19	6	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to A \in P$
20		simp-4r	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to c \in P$
21	3	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to X \in P$
22	4	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to Y \in P$
23	5	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to Z \in P$
24		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
25	9	ad5antr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
26		simpllr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩$
27	1 11 12 13 14 15 21 22 23 24 16 17 20 25 26	ragcgr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ a B c ”⟩ \in ∟_{𝒢} (G)$
28	1 11 12 13 14 15 16 17 20 27	ragcom	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ c B a ”⟩ \in ∟_{𝒢} (G)$
29		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
30		simpr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to c {hl}_{𝒢} (G) (B) C$
31	1 12 29 20 18 17 15 30	hlne1	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to c \neq B$
32	1 12 29 20 18 17 15 30	hlcomd	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to C {hl}_{𝒢} (G) (B) c$
33	1 12 29 18 20 17 15 13 32	hlln	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to C \in (c {Line}_{𝒢} (G) B)$
34	33	orcd	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to (C \in (c {Line}_{𝒢} (G) B) \lor c = B)$
35	1 13 12 15 20 17 18 34	colrot1	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to (c \in (B {Line}_{𝒢} (G) C) \lor B = C)$
36	1 11 12 13 14 15 20 17 16 18 28 31 35	ragcol	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ C B a ”⟩ \in ∟_{𝒢} (G)$
37	1 11 12 13 14 15 18 17 16 36	ragcom	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ a B C ”⟩ \in ∟_{𝒢} (G)$
38		simplr	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to a {hl}_{𝒢} (G) (B) A$
39	1 12 29 16 19 17 15 38	hlne1	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to a \neq B$
40	1 12 29 16 19 17 15 38	hlcomd	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to A {hl}_{𝒢} (G) (B) a$
41	1 12 29 19 16 17 15 13 40	hlln	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to A \in (a {Line}_{𝒢} (G) B)$
42	41	orcd	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to (A \in (a {Line}_{𝒢} (G) B) \lor a = B)$
43	1 13 12 15 16 17 19 42	colrot1	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to (a \in (B {Line}_{𝒢} (G) A) \lor B = A)$
44	1 11 12 13 14 15 16 17 18 19 37 39 43	ragcol	$⊢ (((((φ \land a \in P) \land c \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩) \land a {hl}_{𝒢} (G) (B) A) \land c {hl}_{𝒢} (G) (B) C) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
45	44	3anasss	$⊢ (((φ \land a \in P) \land c \in P) \land (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩ \land a {hl}_{𝒢} (G) (B) A \land c {hl}_{𝒢} (G) (B) C)) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
46	1 12 29 2 3 4 5 6 7 8	iscgra	$⊢ φ \to (⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow \exists a \in P \exists c \in P (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩ \land a {hl}_{𝒢} (G) (B) A \land c {hl}_{𝒢} (G) (B) C))$
47	10 46	mpbid	$⊢ φ \to \exists a \in P \exists c \in P (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ a B c ”⟩ \land a {hl}_{𝒢} (G) (B) A \land c {hl}_{𝒢} (G) (B) C)$
48	45 47	r19.29vva	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem cgrarag

Proof