ragcgr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ragcgr		Structured version Visualization version GIF version

Theorem ragcgr 28225

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
ragcgr	⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩ ∈ (∟G‘𝐺))

**Proof of Theorem ragcgr**
Step	Hyp	Ref	Expression
1		eqidd 2731	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 = 𝐷)
2		israg.p	. . . . 5 ⊢ 𝑃 = (Base‘𝐺)
3		israg.d	. . . . 5 ⊢ − = (dist‘𝐺)
4		israg.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
5		israg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6	5	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐺 ∈ TarskiG)
7		israg.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
8	7	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ 𝑃)
9		israg.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
10	9	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐶 ∈ 𝑃)
11		ragcgr.e	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
12	11	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 ∈ 𝑃)
13		ragcgr.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
14	13	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐹 ∈ 𝑃)
15		ragcgr.c	. . . . . 6 ⊢ ∼ = (cgrG‘𝐺)
16		israg.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
17	16	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐴 ∈ 𝑃)
18		ragcgr.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
19	18	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 ∈ 𝑃)
20		ragcgr.2	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
21	20	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
22	2, 3, 4, 15, 6, 17, 8, 10, 19, 12, 14, 21	cgr3simp2 28039	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = (𝐸 − 𝐹))
23		simpr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
24	2, 3, 4, 6, 8, 10, 12, 14, 22, 23	tgcgreq 28000	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 = 𝐹)
25		eqidd 2731	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐹 = 𝐹)
26	1, 24, 25	s3eqd 14819	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ⟨“𝐷𝐸𝐹”⟩ = ⟨“𝐷𝐹𝐹”⟩)
27		israg.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
28		israg.s	. . . 4 ⊢ 𝑆 = (pInvG‘𝐺)
29	2, 3, 4, 27, 28, 6, 19, 14, 12	ragtrivb 28220	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ⟨“𝐷𝐹𝐹”⟩ ∈ (∟G‘𝐺))
30	26, 29	eqeltrd 2831	. 2 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ⟨“𝐷𝐸𝐹”⟩ ∈ (∟G‘𝐺))
31		ragcgr.1	. . . . . 6 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))
32	31	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))
33	5	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐺 ∈ TarskiG)
34	16	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐴 ∈ 𝑃)
35	7	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ 𝑃)
36	9	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ∈ 𝑃)
37	2, 3, 4, 27, 28, 33, 34, 35, 36	israg 28215	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶))))
38	32, 37	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)))
39	13	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐹 ∈ 𝑃)
40	18	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐷 ∈ 𝑃)
41	11	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ 𝑃)
42	20	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
43	2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42	cgr3simp3 28040	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐴) = (𝐹 − 𝐷))
44	2, 3, 4, 33, 36, 34, 39, 40, 43	tgcgrcomlr 27998	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐶) = (𝐷 − 𝐹))
45		eqid 2730	. . . . . 6 ⊢ (𝑆‘𝐵) = (𝑆‘𝐵)
46	2, 3, 4, 27, 28, 33, 35, 45, 36	mircl 28179	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ((𝑆‘𝐵)‘𝐶) ∈ 𝑃)
47		eqid 2730	. . . . . 6 ⊢ (𝑆‘𝐸) = (𝑆‘𝐸)
48	2, 3, 4, 27, 28, 33, 41, 47, 39	mircl 28179	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ((𝑆‘𝐸)‘𝐹) ∈ 𝑃)
49		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶)
50	49	necomd 2994	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ≠ 𝐵)
51	2, 3, 4, 27, 28, 33, 35, 45, 36	mirbtwn 28176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ (((𝑆‘𝐵)‘𝐶)𝐼𝐶))
52	2, 3, 4, 33, 46, 35, 36, 51	tgbtwncom 28006	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ (𝐶𝐼((𝑆‘𝐵)‘𝐶)))
53	2, 3, 4, 27, 28, 33, 41, 47, 39	mirbtwn 28176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ (((𝑆‘𝐸)‘𝐹)𝐼𝐹))
54	2, 3, 4, 33, 48, 41, 39, 53	tgbtwncom 28006	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ (𝐹𝐼((𝑆‘𝐸)‘𝐹)))
55	2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42	cgr3simp2 28039	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐶) = (𝐸 − 𝐹))
56	2, 3, 4, 33, 35, 36, 41, 39, 55	tgcgrcomlr 27998	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐵) = (𝐹 − 𝐸))
57	2, 3, 4, 27, 28, 33, 35, 45, 36	mircgr 28175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − ((𝑆‘𝐵)‘𝐶)) = (𝐵 − 𝐶))
58	2, 3, 4, 27, 28, 33, 41, 47, 39	mircgr 28175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − ((𝑆‘𝐸)‘𝐹)) = (𝐸 − 𝐹))
59	55, 57, 58	3eqtr4d 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − ((𝑆‘𝐵)‘𝐶)) = (𝐸 − ((𝑆‘𝐸)‘𝐹)))
60	2, 3, 4, 15, 33, 34, 35, 36, 40, 41, 39, 42	cgr3simp1 28038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
61	2, 3, 4, 33, 34, 35, 40, 41, 60	tgcgrcomlr 27998	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐴) = (𝐸 − 𝐷))
62	2, 3, 4, 33, 36, 35, 46, 39, 41, 48, 34, 40, 50, 52, 54, 56, 59, 43, 61	axtg5seg 27983	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (((𝑆‘𝐵)‘𝐶) − 𝐴) = (((𝑆‘𝐸)‘𝐹) − 𝐷))
63	2, 3, 4, 33, 46, 34, 48, 40, 62	tgcgrcomlr 27998	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐴 − ((𝑆‘𝐵)‘𝐶)) = (𝐷 − ((𝑆‘𝐸)‘𝐹)))
64	38, 44, 63	3eqtr3d 2778	. . 3 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐷 − 𝐹) = (𝐷 − ((𝑆‘𝐸)‘𝐹)))
65	2, 3, 4, 27, 28, 33, 40, 41, 39	israg 28215	. . 3 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (⟨“𝐷𝐸𝐹”⟩ ∈ (∟G‘𝐺) ↔ (𝐷 − 𝐹) = (𝐷 − ((𝑆‘𝐸)‘𝐹))))
66	64, 65	mpbird 256	. 2 ⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → ⟨“𝐷𝐸𝐹”⟩ ∈ (∟G‘𝐺))
67	30, 66	pm2.61dane 3027	1 ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩ ∈ (∟G‘𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 class class class wbr 5147 ‘cfv 6542 (class class class)co 7411 ⟨“cs3 14797 Basecbs 17148 distcds 17210 TarskiGcstrkg 27945 Itvcitv 27951 LineGclng 27952 cgrGccgrg 28028 pInvGcmir 28170 ∟Gcrag 28211

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-n0 12477 df-z 12563 df-uz 12827 df-fz 13489 df-fzo 13632 df-hash 14295 df-word 14469 df-concat 14525 df-s1 14550 df-s2 14803 df-s3 14804 df-trkgc 27966 df-trkgb 27967 df-trkgcb 27968 df-trkg 27971 df-cgrg 28029 df-mir 28171 df-rag 28212

This theorem is referenced by: motrag 28226 footexALT 28236 footexlem1 28237 footexlem2 28238

W3C validator