ragcgr

Description: Right angle and colinearity. Theorem 8.10 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 4-Sep-2019)

	Ref	Expression
Hypotheses	israg.p	$⊢ P = {Base}_{G}$
	israg.d	$⊢ \underset{˙}{-} = dist (G)$
	israg.i	$⊢ I = Itv (G)$
	israg.l	$⊢ L = {Line}_{𝒢} (G)$
	israg.s	$⊢ S = {pInv}_{𝒢} (G)$
	israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	israg.a	$⊢ φ \to A \in P$
	israg.b	$⊢ φ \to B \in P$
	israg.c	$⊢ φ \to C \in P$
	ragcgr.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	ragcgr.d	$⊢ φ \to D \in P$
	ragcgr.e	$⊢ φ \to E \in P$
	ragcgr.f	$⊢ φ \to F \in P$
	ragcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	ragcgr.2	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
Assertion	ragcgr	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$⊢ P = {Base}_{G}$
2		israg.d	$⊢ \underset{˙}{-} = dist (G)$
3		israg.i	$⊢ I = Itv (G)$
4		israg.l	$⊢ L = {Line}_{𝒢} (G)$
5		israg.s	$⊢ S = {pInv}_{𝒢} (G)$
6		israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		israg.a	$⊢ φ \to A \in P$
8		israg.b	$⊢ φ \to B \in P$
9		israg.c	$⊢ φ \to C \in P$
10		ragcgr.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
11		ragcgr.d	$⊢ φ \to D \in P$
12		ragcgr.e	$⊢ φ \to E \in P$
13		ragcgr.f	$⊢ φ \to F \in P$
14		ragcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
15		ragcgr.2	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
16		eqidd	$⊢ (φ \land B = C) \to D = D$
17	6	adantr	$⊢ (φ \land B = C) \to G \in 𝒢_{Tarski}$
18	8	adantr	$⊢ (φ \land B = C) \to B \in P$
19	9	adantr	$⊢ (φ \land B = C) \to C \in P$
20	12	adantr	$⊢ (φ \land B = C) \to E \in P$
21	13	adantr	$⊢ (φ \land B = C) \to F \in P$
22	7	adantr	$⊢ (φ \land B = C) \to A \in P$
23	11	adantr	$⊢ (φ \land B = C) \to D \in P$
24	15	adantr	$⊢ (φ \land B = C) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
25	1 2 3 10 17 22 18 19 23 20 21 24	cgr3simp2	$⊢ (φ \land B = C) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
26		simpr	$⊢ (φ \land B = C) \to B = C$
27	1 2 3 17 18 19 20 21 25 26	tgcgreq	$⊢ (φ \land B = C) \to E = F$
28		eqidd	$⊢ (φ \land B = C) \to F = F$
29	16 27 28	s3eqd	$⊢ (φ \land B = C) \to ⟨“ D E F ”⟩ = ⟨“ D F F ”⟩$
30	1 2 3 4 5 17 23 21 20	ragtrivb	$⊢ (φ \land B = C) \to ⟨“ D F F ”⟩ \in ∟_{𝒢} (G)$
31	29 30	eqeltrd	$⊢ (φ \land B = C) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
32	14	adantr	$⊢ (φ \land B \neq C) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
33	6	adantr	$⊢ (φ \land B \neq C) \to G \in 𝒢_{Tarski}$
34	7	adantr	$⊢ (φ \land B \neq C) \to A \in P$
35	8	adantr	$⊢ (φ \land B \neq C) \to B \in P$
36	9	adantr	$⊢ (φ \land B \neq C) \to C \in P$
37	1 2 3 4 5 33 34 35 36	israg	$⊢ (φ \land B \neq C) \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$
38	32 37	mpbid	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C)$
39	13	adantr	$⊢ (φ \land B \neq C) \to F \in P$
40	11	adantr	$⊢ (φ \land B \neq C) \to D \in P$
41	12	adantr	$⊢ (φ \land B \neq C) \to E \in P$
42	15	adantr	$⊢ (φ \land B \neq C) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
43	1 2 3 10 33 34 35 36 40 41 39 42	cgr3simp3	$⊢ (φ \land B \neq C) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
44	1 2 3 33 36 34 39 40 43	tgcgrcomlr	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
45		eqid	$⊢ S (B) = S (B)$
46	1 2 3 4 5 33 35 45 36	mircl	$⊢ (φ \land B \neq C) \to S (B) (C) \in P$
47		eqid	$⊢ S (E) = S (E)$
48	1 2 3 4 5 33 41 47 39	mircl	$⊢ (φ \land B \neq C) \to S (E) (F) \in P$
49		simpr	$⊢ (φ \land B \neq C) \to B \neq C$
50	49	necomd	$⊢ (φ \land B \neq C) \to C \neq B$
51	1 2 3 4 5 33 35 45 36	mirbtwn	$⊢ (φ \land B \neq C) \to B \in (S (B) (C) I C)$
52	1 2 3 33 46 35 36 51	tgbtwncom	$⊢ (φ \land B \neq C) \to B \in (C I S (B) (C))$
53	1 2 3 4 5 33 41 47 39	mirbtwn	$⊢ (φ \land B \neq C) \to E \in (S (E) (F) I F)$
54	1 2 3 33 48 41 39 53	tgbtwncom	$⊢ (φ \land B \neq C) \to E \in (F I S (E) (F))$
55	1 2 3 10 33 34 35 36 40 41 39 42	cgr3simp2	$⊢ (φ \land B \neq C) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
56	1 2 3 33 35 36 41 39 55	tgcgrcomlr	$⊢ (φ \land B \neq C) \to C \underset{˙}{-} B = F \underset{˙}{-} E$
57	1 2 3 4 5 33 35 45 36	mircgr	$⊢ (φ \land B \neq C) \to B \underset{˙}{-} S (B) (C) = B \underset{˙}{-} C$
58	1 2 3 4 5 33 41 47 39	mircgr	$⊢ (φ \land B \neq C) \to E \underset{˙}{-} S (E) (F) = E \underset{˙}{-} F$
59	55 57 58	3eqtr4d	$⊢ (φ \land B \neq C) \to B \underset{˙}{-} S (B) (C) = E \underset{˙}{-} S (E) (F)$
60	1 2 3 10 33 34 35 36 40 41 39 42	cgr3simp1	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
61	1 2 3 33 34 35 40 41 60	tgcgrcomlr	$⊢ (φ \land B \neq C) \to B \underset{˙}{-} A = E \underset{˙}{-} D$
62	1 2 3 33 36 35 46 39 41 48 34 40 50 52 54 56 59 43 61	axtg5seg	$⊢ (φ \land B \neq C) \to S (B) (C) \underset{˙}{-} A = S (E) (F) \underset{˙}{-} D$
63	1 2 3 33 46 34 48 40 62	tgcgrcomlr	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} S (B) (C) = D \underset{˙}{-} S (E) (F)$
64	38 44 63	3eqtr3d	$⊢ (φ \land B \neq C) \to D \underset{˙}{-} F = D \underset{˙}{-} S (E) (F)$
65	1 2 3 4 5 33 40 41 39	israg	$⊢ (φ \land B \neq C) \to (⟨“ D E F ”⟩ \in ∟_{𝒢} (G) \leftrightarrow D \underset{˙}{-} F = D \underset{˙}{-} S (E) (F))$
66	64 65	mpbird	$⊢ (φ \land B \neq C) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
67	31 66	pm2.61dane	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem ragcgr

Proof