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 29059

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 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐺 ∈ TarskiG)
6		lnxfr.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐴 ∈ 𝑃)
8		lnxfr.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
9	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐶 ∈ 𝑃)
10		lnxfr.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
11	10	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ 𝑃)
12		eqid 2763	. . . 4 ⊢ (dist‘𝐺) = (dist‘𝐺)
13		lnxfr.r	. . . 4 ⊢ ∼ = (cgrG‘𝐺)
14		tglngval.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
15	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋 ∈ 𝑃)
16		tglngval.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17	16	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ 𝑃)
18		tgcolg.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19	18	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑍 ∈ 𝑃)
20		lnxfr.2	. . . . 5 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
21	20	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
22		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ (𝑋𝐼𝑍))
23	1, 12, 3, 13, 5, 15, 17, 19, 7, 11, 9, 21, 22	tgbtwnxfr 29023	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ (𝐴𝐼𝐶))
24	1, 2, 3, 5, 7, 9, 11, 23	btwncolg1 29048	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
25	4	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐺 ∈ TarskiG)
26	6	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ 𝑃)
27	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐶 ∈ 𝑃)
28	10	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐵 ∈ 𝑃)
29	16	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑌 ∈ 𝑃)
30	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ 𝑃)
31	18	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑍 ∈ 𝑃)
32	20	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
33	1, 12, 3, 13, 25, 30, 29, 31, 26, 28, 27, 32	cgr3swap12 29016	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → ⟨“𝑌𝑋𝑍”⟩ ∼ ⟨“𝐵𝐴𝐶”⟩)
34		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ (𝑌𝐼𝑍))
35	1, 12, 3, 13, 25, 29, 30, 31, 28, 26, 27, 33, 34	tgbtwnxfr 29023	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ (𝐵𝐼𝐶))
36	1, 2, 3, 25, 26, 27, 28, 35	btwncolg2 29049	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
37	4	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐺 ∈ TarskiG)
38	6	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐴 ∈ 𝑃)
39	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ 𝑃)
40	10	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐵 ∈ 𝑃)
41	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝑃)
42	18	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ 𝑃)
43	16	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝑃)
44	20	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
45	1, 12, 3, 13, 37, 41, 43, 42, 38, 40, 39, 44	cgr3swap23 29017	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → ⟨“𝑋𝑍𝑌”⟩ ∼ ⟨“𝐴𝐶𝐵”⟩)
46		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ (𝑋𝐼𝑌))
47	1, 12, 3, 13, 37, 41, 42, 43, 38, 39, 40, 45, 46	tgbtwnxfr 29023	. . 3 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ (𝐴𝐼𝐵))
48	1, 2, 3, 37, 38, 39, 40, 47	btwncolg3 29050	. 2 ⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
49		lnxfr.1	. . 3 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))
50	1, 2, 3, 4, 14, 18, 16	tgcolg 29047	. . 3 ⊢ (𝜑 → ((𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍) ↔ (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌))))
51	49, 50	mpbid 235	. 2 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌)))
52	24, 36, 48, 51	mpjao3dan 1460	1 ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 = wceq 1570 ∈ wcel 2147 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ⟨“cs3 15021 Basecbs 17416 distcds 17466 TarskiGcstrkg 28919 Itvcitv 28925 LineGclng 28926 cgrGccgrg 29003

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-oadd 8508 df-er 8745 df-pm 8878 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-dju 10009 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-2 12432 df-3 12433 df-n0 12634 df-xnn0 12707 df-z 12721 df-uz 12993 df-fz 13667 df-fzo 13816 df-hash 14502 df-word 14686 df-concat 14743 df-s1 14770 df-s2 15027 df-s3 15028 df-trkgc 28940 df-trkgb 28941 df-trkgcb 28942 df-trkg 28945 df-cgrg 29004

This theorem is used by: symquadlem 29191 midexlem 29194 trgcopy 29341

W3C validator