Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	israg.d	⊢ − = ( dist ‘ 𝐺 )
	israg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	israg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	israg.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	israg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	israg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	israg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	israg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	ragflat.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
	ragflat.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
Assertion	ragflat	⊢ ( 𝜑 → 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		israg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		israg.d	⊢ − = ( dist ‘ 𝐺 )
3		israg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		israg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		israg.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		israg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		israg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		israg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		israg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10		ragflat.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11		ragflat.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
16	9	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
17		eqid	⊢ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 )
18	1 2 3 4 5 13 16 17 14	mircl	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝑃 )
19	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
20	1 2 3 4 5 13 16 17 14	mircgr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) = ( 𝐶 − 𝐴 ) )
21	1 2 3 13 16 18 16 14 20	tgcgrcomlr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − 𝐶 ) = ( 𝐴 − 𝐶 ) )
22	1 2 3 4 5 13 14 15 16	israg	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )
23	19 22	mpbid	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
24		eqid	⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
25	1 2 3 4 5 13 15 24 16	mircl	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
26	11	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
27	1 2 3 4 5 13 14 16 15 26	ragcom	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
29	1 2 3 4 5 13 15 24 16	mirbtwn	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) 𝐼 𝐶 ) )
30	1 2 3 13 25 15 16 29	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
31	1 4 3 13 16 25 15 30	btwncolg1	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 ∈ ( 𝐶 𝐿 ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ∨ 𝐶 = ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
32	1 2 3 4 5 13 15 16 14 25 27 28 31	ragcol	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) 𝐶 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
33	1 2 3 4 5 13 25 16 14	israg	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ⟨“ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) 𝐶 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) ) )
34	32 33	mpbid	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) )
35	1 2 3 13 25 14 25 18 34	tgcgrcomlr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
36	21 23 35	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − 𝐶 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
37	1 2 3 4 5 13 18 15 16	israg	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ⟨“ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − 𝐶 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )
38	36 37	mpbird	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
39	1 2 3 4 5 13 16 17 14	mirbtwn	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) 𝐼 𝐴 ) )
40	1 2 3 13 18 16 14 39	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐴 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) )
41	1 2 3 4 5 13 14 15 16 18 19 38 40	ragflat2	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 = 𝐶 )
42	12 41	pm2.61dane	⊢ ( 𝜑 → 𝐵 = 𝐶 )