Metamath Proof Explorer

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

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 ragcgr.c ⊢ ∼ = ( cgrG ‘ 𝐺 )
11 ragcgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
12 ragcgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
13 ragcgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
14 ragcgr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
15 ragcgr.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
16 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐷 = 𝐷 )
17 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐺 ∈ TarskiG )
18 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ 𝑃 )
19 9 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐶 ∈ 𝑃 )
20 12 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐸 ∈ 𝑃 )
21 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐹 ∈ 𝑃 )
22 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐴 ∈ 𝑃 )
23 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐷 ∈ 𝑃 )
24 15 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
25 1 2 3 10 17 22 18 19 23 20 21 24 cgr3simp2 ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
27 1 2 3 17 18 19 20 21 25 26 tgcgreq ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐸 = 𝐹 )
28 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐹 = 𝐹 )
29 16 27 28 s3eqd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ = ⟨“ 𝐷 𝐹 𝐹 ”⟩ )
30 1 2 3 4 5 17 23 21 20 ragtrivb ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ⟨“ 𝐷 𝐹 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
31 29 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
32 14 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
33 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
34 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
35 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
36 9 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
37 1 2 3 4 5 33 34 35 36 israg ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )
38 32 37 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
39 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐹 ∈ 𝑃 )
40 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐷 ∈ 𝑃 )
41 12 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐸 ∈ 𝑃 )
42 15 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
43 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp3 ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
44 1 2 3 33 36 34 39 40 43 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
45 eqid ⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
46 1 2 3 4 5 33 35 45 36 mircl ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
47 eqid ⊢ ( 𝑆 ‘ 𝐸 ) = ( 𝑆 ‘ 𝐸 )
48 1 2 3 4 5 33 41 47 39 mircl ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ∈ 𝑃 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
50 49 necomd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ≠ 𝐵 )
51 1 2 3 4 5 33 35 45 36 mirbtwn ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) 𝐼 𝐶 ) )
52 1 2 3 33 46 35 36 51 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
53 1 2 3 4 5 33 41 47 39 mirbtwn ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐸 ∈ ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) 𝐼 𝐹 ) )
54 1 2 3 33 48 41 39 53 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐸 ∈ ( 𝐹 𝐼 ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) )
55 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp2 ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
56 1 2 3 33 35 36 41 39 55 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝐸 ) )
57 1 2 3 4 5 33 35 45 36 mircgr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( 𝐵 − 𝐶 ) )
58 1 2 3 4 5 33 41 47 39 mircgr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐸 − ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) = ( 𝐸 − 𝐹 ) )
59 55 57 58 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( 𝐸 − ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) )
60 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp1 ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
61 1 2 3 33 34 35 40 41 60 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
62 1 2 3 33 36 35 46 39 41 48 34 40 50 52 54 56 59 43 61 axtg5seg ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) − 𝐷 ) )
63 1 2 3 33 46 34 48 40 62 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( 𝐷 − ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) )
64 38 44 63 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐷 − 𝐹 ) = ( 𝐷 − ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) )
65 1 2 3 4 5 33 40 41 39 israg ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐷 − 𝐹 ) = ( 𝐷 − ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐹 ) ) ) )
66 64 65 mpbird ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
67 31 66 pm2.61dane ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )