lnxfr - Metamath Proof Explorer

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

Theorem lnxfr 28622

Description: Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)

**Hypotheses**
Ref	Expression
tglngval.p	⊢ 𝑃 = (Base‘𝐺)
tglngval.l	⊢ 𝐿 = (LineG‘𝐺)
tglngval.i	⊢ 𝐼 = (Itv‘𝐺)
tglngval.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tglngval.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
tglngval.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
tgcolg.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)
lnxfr.r	⊢ ∼ = (cgrG‘𝐺)
lnxfr.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
lnxfr.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
lnxfr.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
lnxfr.1	⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))
lnxfr.2	⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)

**Assertion**
Ref	Expression
lnxfr	⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))

**Proof of Theorem lnxfr**
Step	Hyp	Ref	Expression
1		tglngval.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		tglngval.l	. . 3 ⊢ 𝐿 = (LineG‘𝐺)
3		tglngval.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
4		tglngval.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐺 ∈ TarskiG)
6		lnxfr.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐴 ∈ 𝑃)
8		lnxfr.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
9	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐶 ∈ 𝑃)
10		lnxfr.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
11	10	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ 𝑃)
12		eqid 2737	. . . 4 ⊢ (dist‘𝐺) = (dist‘𝐺)
13		lnxfr.r	. . . 4 ⊢ ∼ = (cgrG‘𝐺)
14		tglngval.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
15	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋 ∈ 𝑃)
16		tglngval.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ 𝑃)
18		tgcolg.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑍 ∈ 𝑃)
20		lnxfr.2	. . . . 5 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
21	20	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
22		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ (𝑋𝐼𝑍))
23	1, 12, 3, 13, 5, 15, 17, 19, 7, 11, 9, 21, 22	tgbtwnxfr 28586	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ (𝐴𝐼𝐶))
24	1, 2, 3, 5, 7, 9, 11, 23	btwncolg1 28611	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
25	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐺 ∈ TarskiG)
26	6	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ 𝑃)
27	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐶 ∈ 𝑃)
28	10	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐵 ∈ 𝑃)
29	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑌 ∈ 𝑃)
30	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ 𝑃)
31	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑍 ∈ 𝑃)
32	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
33	1, 12, 3, 13, 25, 30, 29, 31, 26, 28, 27, 32	cgr3swap12 28579	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → ⟨“𝑌𝑋𝑍”⟩ ∼ ⟨“𝐵𝐴𝐶”⟩)
34		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ (𝑌𝐼𝑍))
35	1, 12, 3, 13, 25, 29, 30, 31, 28, 26, 27, 33, 34	tgbtwnxfr 28586	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ (𝐵𝐼𝐶))
36	1, 2, 3, 25, 26, 27, 28, 35	btwncolg2 28612	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
37	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐺 ∈ TarskiG)
38	6	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐴 ∈ 𝑃)
39	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ 𝑃)
40	10	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐵 ∈ 𝑃)
41	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝑃)
42	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ 𝑃)
43	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝑃)
44	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
45	1, 12, 3, 13, 37, 41, 43, 42, 38, 40, 39, 44	cgr3swap23 28580	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → ⟨“𝑋𝑍𝑌”⟩ ∼ ⟨“𝐴𝐶𝐵”⟩)
46		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ (𝑋𝐼𝑌))
47	1, 12, 3, 13, 37, 41, 42, 43, 38, 39, 40, 45, 46	tgbtwnxfr 28586	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ (𝐴𝐼𝐵))
48	1, 2, 3, 37, 38, 39, 40, 47	btwncolg3 28613	. 2 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
49		lnxfr.1	. . 3 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))
50	1, 2, 3, 4, 14, 18, 16	tgcolg 28610	. . 3 ⊢ (𝜑 → ((𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍) ↔ (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌))))
51	49, 50	mpbid 232	. 2 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌)))
52	24, 36, 48, 51	mpjao3dan 1435	1 ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 848 ∨ w3o 1086 = wceq 1542 ∈ wcel 2114 class class class wbr 5086 ‘cfv 6490 (class class class)co 7358 ⟨“cs3 14766 Basecbs 17137 distcds 17187 TarskiGcstrkg 28483 Itvcitv 28489 LineGclng 28490 cgrGccgrg 28566

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-oadd 8400 df-er 8634 df-pm 8767 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-dju 9814 df-card 9852 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-3 12210 df-n0 12403 df-xnn0 12476 df-z 12490 df-uz 12753 df-fz 13425 df-fzo 13572 df-hash 14255 df-word 14438 df-concat 14495 df-s1 14521 df-s2 14772 df-s3 14773 df-trkgc 28504 df-trkgb 28505 df-trkgcb 28506 df-trkg 28509 df-cgrg 28567

This theorem is referenced by: symquadlem 28745 midexlem 28748 trgcopy 28860

W3C validator