ragflat

Description: Deduce equality from two right angles. Theorem 8.7 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 3-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$
	ragflat.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	ragflat.2	$⊢ φ \to ⟨“ A C B ”⟩ \in ∟_{𝒢} (G)$
Assertion	ragflat	$⊢ φ \to B = C$

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		ragflat.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
11		ragflat.2	$⊢ φ \to ⟨“ A C B ”⟩ \in ∟_{𝒢} (G)$
12		simpr	$⊢ (φ \land B = C) \to B = C$
13	6	adantr	$⊢ (φ \land B \neq C) \to G \in 𝒢_{Tarski}$
14	7	adantr	$⊢ (φ \land B \neq C) \to A \in P$
15	8	adantr	$⊢ (φ \land B \neq C) \to B \in P$
16	9	adantr	$⊢ (φ \land B \neq C) \to C \in P$
17		eqid	$⊢ S (C) = S (C)$
18	1 2 3 4 5 13 16 17 14	mircl	$⊢ (φ \land B \neq C) \to S (C) (A) \in P$
19	10	adantr	$⊢ (φ \land B \neq C) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
20	1 2 3 4 5 13 16 17 14	mircgr	$⊢ (φ \land B \neq C) \to C \underset{˙}{-} S (C) (A) = C \underset{˙}{-} A$
21	1 2 3 13 16 18 16 14 20	tgcgrcomlr	$⊢ (φ \land B \neq C) \to S (C) (A) \underset{˙}{-} C = A \underset{˙}{-} C$
22	1 2 3 4 5 13 14 15 16	israg	$⊢ (φ \land B \neq C) \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$
23	19 22	mpbid	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C)$
24		eqid	$⊢ S (B) = S (B)$
25	1 2 3 4 5 13 15 24 16	mircl	$⊢ (φ \land B \neq C) \to S (B) (C) \in P$
26	11	adantr	$⊢ (φ \land B \neq C) \to ⟨“ A C B ”⟩ \in ∟_{𝒢} (G)$
27	1 2 3 4 5 13 14 16 15 26	ragcom	$⊢ (φ \land B \neq C) \to ⟨“ B C A ”⟩ \in ∟_{𝒢} (G)$
28		simpr	$⊢ (φ \land B \neq C) \to B \neq C$
29	1 2 3 4 5 13 15 24 16	mirbtwn	$⊢ (φ \land B \neq C) \to B \in (S (B) (C) I C)$
30	1 2 3 13 25 15 16 29	tgbtwncom	$⊢ (φ \land B \neq C) \to B \in (C I S (B) (C))$
31	1 4 3 13 16 25 15 30	btwncolg1	$⊢ (φ \land B \neq C) \to (B \in (C L S (B) (C)) \lor C = S (B) (C))$
32	1 2 3 4 5 13 15 16 14 25 27 28 31	ragcol	$⊢ (φ \land B \neq C) \to ⟨“ S (B) (C) C A ”⟩ \in ∟_{𝒢} (G)$
33	1 2 3 4 5 13 25 16 14	israg	$⊢ (φ \land B \neq C) \to (⟨“ S (B) (C) C A ”⟩ \in ∟_{𝒢} (G) \leftrightarrow S (B) (C) \underset{˙}{-} A = S (B) (C) \underset{˙}{-} S (C) (A))$
34	32 33	mpbid	$⊢ (φ \land B \neq C) \to S (B) (C) \underset{˙}{-} A = S (B) (C) \underset{˙}{-} S (C) (A)$
35	1 2 3 13 25 14 25 18 34	tgcgrcomlr	$⊢ (φ \land B \neq C) \to A \underset{˙}{-} S (B) (C) = S (C) (A) \underset{˙}{-} S (B) (C)$
36	21 23 35	3eqtrd	$⊢ (φ \land B \neq C) \to S (C) (A) \underset{˙}{-} C = S (C) (A) \underset{˙}{-} S (B) (C)$
37	1 2 3 4 5 13 18 15 16	israg	$⊢ (φ \land B \neq C) \to (⟨“ S (C) (A) B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow S (C) (A) \underset{˙}{-} C = S (C) (A) \underset{˙}{-} S (B) (C))$
38	36 37	mpbird	$⊢ (φ \land B \neq C) \to ⟨“ S (C) (A) B C ”⟩ \in ∟_{𝒢} (G)$
39	1 2 3 4 5 13 16 17 14	mirbtwn	$⊢ (φ \land B \neq C) \to C \in (S (C) (A) I A)$
40	1 2 3 13 18 16 14 39	tgbtwncom	$⊢ (φ \land B \neq C) \to C \in (A I S (C) (A))$
41	1 2 3 4 5 13 14 15 16 18 19 38 40	ragflat2	$⊢ (φ \land B \neq C) \to B = C$
42	12 41	pm2.61dane	$⊢ φ \to B = C$

Metamath Proof Explorer

Theorem ragflat

Proof